1 /-
2 Copyright (c) 2018 Patrick Massot. All rights reserved.
3 Released under Apache 2.0 license as described in the file LICENSE.
4 Authors: Patrick Massot, Johannes Hölzl
5
6 Uniform structure on topological groups:
7
8 * `topological_add_group.to_uniform_space` and `topological_add_group_is_uniform` can be used to
9 construct a canonical uniformity for a topological add group.
10
11 * extension of ℤ-bilinear maps to complete groups (useful for ring completions)
12
13 * `add_group_with_zero_nhd`: construct the topological structure from a group with a neighbourhood
14 around zero. Then with `topological_add_group.to_uniform_space` one can derive a `uniform_space`.
15 -/
16 import topology.uniform_space.uniform_embedding topology.uniform_space.complete_separated
src └──────────────────────────────────────┘ └───────────────────────────────────────┘
17 import topology.algebra.group
src └────────────────────┘
18
19 noncomputable theory
20 open_locale classical uniformity topological_space
21
22 section uniform_add_group
23 open filter set
24
25 variables {α : Type*} {β : Type*}
26
27 /-- A uniform (additive) group is a group in which the addition and negation are
28 uniformly continuous. -/
29 class uniform_add_group (α : Type*) [uniform_space α] [add_group α] : Prop :=
id └───┘ └───────────┘ ┴ └───────┘ ┴
src └───────────┘ └───────┘
typ └───┘ └───────────┘ ┴ └───────┘ ┴
doc └───────────┘
30 (uniform_continuous_sub : uniform_continuous (λp:α×α, p.1 - p.2))
id └────────────────┘ ┴┴┴ ┴┴ ┴ ┴┴
src └────────────────┘ ┴ ┴ ┴ ┴
typ └────────────────┘ ┴┴┴ ┴┴ ┴ ┴┴
31
32 theorem uniform_add_group.mk' {α} [uniform_space α] [add_group α]
id └───────────┘ ┴ └───────┘ ┴
src └───────────┘ └───────┘
typ └───────────┘ ┴ └───────┘ ┴
doc └───────────┘
33 (h₁ : uniform_continuous (λp:α×α, p.1 + p.2))
id └────────────────┘ ┴┴┴ ┴┴ ┴ ┴┴
src └────────────────┘ ┴ ┴ ┴ ┴
typ └────────────────┘ ┴┴┴ ┴┴ ┴ ┴┴
34 (h₂ : uniform_continuous (λp:α, -p)) : uniform_add_group α :=
id └────────────────┘ ┴ ┴┴ └───────────────┘ ┴
src └────────────────┘ ┴ └───────────────┘
typ └────────────────┘ ┴ ┴┴ └───────────────┘ ┴
doc └───────────────┘
35 ⟨h₁.comp (uniform_continuous_fst.prod_mk (h₂.comp uniform_continuous_snd))⟩
id └┘└───┘ └────────────────────┘└──────┘ └┘└───┘ └────────────────────┘
src └───┘ └────────────────────┘└──────┘ └───┘ └────────────────────┘
typ └┘└───┘ └────────────────────┘└──────┘ └┘└───┘ └────────────────────┘
36
37 variables [uniform_space α] [add_group α] [uniform_add_group α]
id └───────────┘ ┴└───────┘ └───────────────┘
src └───────────┘ └───────┘ └───────────────┘
typ └───────────┘ ┴└───────┘ └───────────────┘
doc └───────────┘ └───────────────┘
38
39 lemma uniform_continuous_sub : uniform_continuous (λp:α×α, p.1 - p.2) :=
id └────────────────┘ ┴┴┴ ┴┴ ┴ ┴┴
src └────────────────┘ ┴ ┴ ┴ ┴
typ └────────────────┘ ┴┴┴ ┴┴ ┴ ┴┴
40 uniform_add_group.uniform_continuous_sub α
id └──────────────────────────────────────┘ ┴
src └──────────────────────────────────────┘
typ └──────────────────────────────────────┘ ┴
41
42 lemma uniform_continuous.sub [uniform_space β] {f : β → α} {g : β → α}
id └───────────┘ ┴ ┴ ┴ ┴ ┴
src └───────────┘
typ └───────────┘ ┴ ┴ ┴ ┴ ┴
doc └───────────┘
43 (hf : uniform_continuous f) (hg : uniform_continuous g) : uniform_continuous (λx, f x - g x) :=
id └────────────────┘ ┴ └────────────────┘ ┴ └────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴
src └────────────────┘ └────────────────┘ └────────────────┘ ┴
typ └────────────────┘ ┴ └────────────────┘ ┴ └────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴
44 uniform_continuous_sub.comp (hf.prod_mk hg)
id └────────────────────┘└───┘ └┘└──────┘ └┘
src └────────────────────┘└───┘ └──────┘
typ └────────────────────┘└───┘ └┘└──────┘ └┘
45
46 lemma uniform_continuous.neg [uniform_space β] {f : β → α}
id └───────────┘ ┴ ┴ ┴
src └───────────┘
typ └───────────┘ ┴ ┴ ┴
doc └───────────┘
47 (hf : uniform_continuous f) : uniform_continuous (λx, - f x) :=
id └────────────────┘ ┴ └────────────────┘ ┴ ┴ ┴ ┴
src └────────────────┘ └────────────────┘ ┴
typ └────────────────┘ ┴ └────────────────┘ ┴ ┴ ┴ ┴
48 have uniform_continuous (λx, 0 - f x),
id └────────────────┘ ┴ ┴ ┴ ┴
src └────────────────┘ ┴
typ └────────────────┘ ┴ ┴ ┴ ┴
49 from uniform_continuous_const.sub hf,
id └──────────────────────┘└──┘ └┘
src └──────────────────────┘└──┘
typ └──────────────────────┘└──┘ └┘
50 by simp * at *
src └───────────
typ └───────────
doc └───────────
txt └───────────
par └───────────
pid ┴┴┴└──┘└
st └────────────
51
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
52 lemma uniform_continuous_neg : uniform_continuous (λx:α, - x) :=
id └────────────────┘ ┴ ┴ ┴
src └────────────────┘ ┴
typ └────────────────┘ ┴ ┴ ┴
53 uniform_continuous_id.neg
id └───────────────────┘└──┘
src └───────────────────┘└──┘
typ └───────────────────┘└──┘
54
55 lemma uniform_continuous.add [uniform_space β] {f : β → α} {g : β → α}
id └───────────┘ ┴ ┴ ┴ ┴ ┴
src └───────────┘
typ └───────────┘ ┴ ┴ ┴ ┴ ┴
doc └───────────┘
56 (hf : uniform_continuous f) (hg : uniform_continuous g) : uniform_continuous (λx, f x + g x) :=
id └────────────────┘ ┴ └────────────────┘ ┴ └────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴
src └────────────────┘ └────────────────┘ └────────────────┘ ┴
typ └────────────────┘ ┴ └────────────────┘ ┴ └────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴
57 have uniform_continuous (λx, f x - - g x), from hf.sub hg.neg,
id └────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘└──┘ └┘└──┘
src └────────────────┘ ┴ ┴ └──┘ └──┘
typ └────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘└──┘ └┘└──┘
58 by simp * at *
src └───────────
typ └───────────
doc └───────────
txt └───────────
par └───────────
pid ┴┴┴└──┘└
st └────────────
59
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
60 lemma uniform_continuous_add : uniform_continuous (λp:α×α, p.1 + p.2) :=
id └────────────────┘ ┴┴┴ ┴┴ ┴ ┴┴
src └────────────────┘ ┴ ┴ ┴ ┴
typ └────────────────┘ ┴┴┴ ┴┴ ┴ ┴┴
61 uniform_continuous_fst.add uniform_continuous_snd
id └────────────────────┘└──┘ └────────────────────┘
src └────────────────────┘└──┘ └────────────────────┘
typ └────────────────────┘└──┘ └────────────────────┘
62
63 @[priority 10]
64 instance uniform_add_group.to_topological_add_group : topological_add_group α :=
id └───────────────────┘ ┴
src └───────────────────┘
typ └───────────────────┘ ┴
doc └───────────────────┘
65 { continuous_add := uniform_continuous_add.continuous,
id └────────────────────┘└─────────┘
src └────────────────────┘└─────────┘
typ └────────────────────┘└─────────┘
66 continuous_neg := uniform_continuous_neg.continuous }
id └────────────────────┘└─────────┘
src └────────────────────┘└─────────┘
typ └────────────────────┘└─────────┘
67
68 instance [uniform_space β] [add_group β] [uniform_add_group β] : uniform_add_group (α × β) :=
id └───────────┘ ┴ └───────┘ ┴ └───────────────┘ ┴ └───────────────┘ ┴ ┴ ┴
src └───────────┘ └───────┘ └───────────────┘ └───────────────┘ ┴
typ └───────────┘ ┴ └───────┘ ┴ └───────────────┘ ┴ └───────────────┘ ┴ ┴ ┴
doc └───────────┘ └───────────────┘ └───────────────┘
69 ⟨((uniform_continuous_fst.comp uniform_continuous_fst).sub
id └────────────────────┘└───┘ └────────────────────┘ └─┘
src └────────────────────┘└───┘ └────────────────────┘ └─┘
typ └────────────────────┘└───┘ └────────────────────┘ └─┘
70 (uniform_continuous_fst.comp uniform_continuous_snd)).prod_mk
id └────────────────────┘└───┘ └────────────────────┘ └─────┘
src └────────────────────┘└───┘ └────────────────────┘ └─────┘
typ └────────────────────┘└───┘ └────────────────────┘ └─────┘
71 ((uniform_continuous_snd.comp uniform_continuous_fst).sub
id └────────────────────┘└───┘ └────────────────────┘ └─┘
src └────────────────────┘└───┘ └────────────────────┘ └─┘
typ └────────────────────┘└───┘ └────────────────────┘ └─┘
72 (uniform_continuous_snd.comp uniform_continuous_snd))⟩
id └────────────────────┘└───┘ └────────────────────┘
src └────────────────────┘└───┘ └────────────────────┘
typ └────────────────────┘└───┘ └────────────────────┘
73
74 lemma uniformity_translate (a : α) : (𝓤 α).map (λx:α×α, (x.1 + a, x.2 + a)) = 𝓤 α :=
id ┴ ┴ ┴ └─┘ ┴┴┴ ┴┴┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴
src ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ └─┘ ┴┴┴ ┴┴┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴
doc ┴ └─┘ ┴
75 le_antisymm
id └─────────┘
src └─────────┘
typ └─────────┘
76 (uniform_continuous_id.add uniform_continuous_const)
id └───────────────────┘└──┘ └──────────────────────┘
src └───────────────────┘└──┘ └──────────────────────┘
typ └───────────────────┘└──┘ └──────────────────────┘
77 (calc 𝓤 α =
id ┴ ┴
src ┴
typ ┴ ┴
doc ┴
78 ((𝓤 α).map (λx:α×α, (x.1 + -a, x.2 + -a))).map (λx:α×α, (x.1 + a, x.2 + a)) :
id ┴ ┴ └─┘ ┴┴┴ ┴┴┴ ┴ ┴┴ ┴┴ ┴ ┴┴ └─┘ ┴┴┴ ┴┴┴ ┴ ┴ ┴┴ ┴ ┴
src ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ └─┘ ┴┴┴ ┴┴┴ ┴ ┴┴ ┴┴ ┴ ┴┴ └─┘ ┴┴┴ ┴┴┴ ┴ ┴ ┴┴ ┴ ┴
doc ┴ └─┘ └─┘
79 by simp [filter.map_map, (∘)]; exact filter.map_id.symm
id └────────────┘ ┴ └────────────────┘
src └────┘└────────────┘└┘┴└─┘ └────┘└────────────────┘└
typ └────┘└────────────┘└┘┴└─┘ └────┘└────────────────┘└
doc └────┘ └┘ └─┘ └────┘ └
txt └────┘ └┘ └─┘ └────┘ └
par └────┘ └┘ └─┘ └────┘ └
pid ┴┴ └┘ └─┘ ┴ └
st └─────────────────────────────────────────────────────
80 ... ≤ (𝓤 α).map (λx:α×α, (x.1 + a, x.2 + a)) :
id ┴ ┴ └─┘ ┴┴┴ ┴┴┴ ┴ ┴ ┴┴ ┴ ┴
src ───┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴
typ ───┘ ┴ ┴ └─┘ ┴┴┴ ┴┴┴ ┴ ┴ ┴┴ ┴ ┴
doc ───┘ ┴ └─┘
txt ───┘
par ───┘
pid ───┘
st ───┘
81 filter.map_mono (uniform_continuous_id.add uniform_continuous_const))
id └─────────────┘ └───────────────────┘└──┘ └──────────────────────┘
src └─────────────┘ └───────────────────┘└──┘ └──────────────────────┘
typ └─────────────┘ └───────────────────┘└──┘ └──────────────────────┘
82
83 lemma uniform_embedding_translate (a : α) : uniform_embedding (λx:α, x + a) :=
id ┴ └───────────────┘ ┴ ┴ ┴ ┴
src └───────────────┘ ┴
typ ┴ └───────────────┘ ┴ ┴ ┴ ┴
84 { comap_uniformity := begin
st └─────
85 rw [← uniformity_translate a, comap_map] {occs := occurrences.pos [1]},
id └──────────────────┘ ┴ └───────┘ └─────────────┘ ┴ ┴
src └────┘└──────────────────┘┴ └┘└───────┘└┘ └──────┘└─────────────┘┴┴┴┴┴
typ └────┘└──────────────────┘┴┴└┘└───────┘└┘ └──────┘└─────────────┘┴┴┴┴┴
doc └────┘ ┴ └┘ └┘ └──────┘ ┴ ┴ ┴
txt └────┘ ┴ └┘ └┘ └──────┘ ┴ ┴ ┴
par └────┘ ┴ └┘ └┘ └──────┘ ┴ ┴ ┴
pid └──┘ ┴ └┘ ┴┴ └──────┘ ┴ ┴ ┴
st ───────────────────────────────┘└─────────┘┴└────────────────────────────┘└─
86 rintros ⟨p₁, p₂⟩ ⟨q₁, q₂⟩,
src └───────────────────────┘
typ └───────────────────────┘
doc └───────────────────────┘
txt └───────────────────────┘
par └───────────────────────┘
pid └────────────────┘
st ────────────────────────────┘└─
87 simp [prod.eq_iff_fst_eq_snd_eq] {contextual := tt}
id └───────────────────────┘ └┘
src └────┘└───────────────────────┘└┘ └────────────┘└┘└─
typ └────┘└───────────────────────┘└┘ └────────────┘└┘└─
doc └────┘ └┘ └────────────┘ └─
txt └────┘ └┘ └────────────┘ └─
par └────┘ └┘ └────────────┘ └─
pid ┴┴ ┴┴ └────────────┘ ┴└
st ────────────────────────────────────────────────────────
88 end,
src ─┘
typ ─┘
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘└─┘
89 inj := assume x y, eq_of_add_eq_add_right }
id ┴ ┴ └────────────────────┘
src └────────────────────┘
typ ┴ ┴ └────────────────────┘
90
91 section
92 variables (α)
93 lemma uniformity_eq_comap_nhds_zero : 𝓤 α = comap (λx:α×α, x.2 - x.1) (𝓝 (0:α)) :=
id ┴ ┴ ┴ └───┘ ┴┴┴ ┴┴ ┴ ┴┴ ┴ ┴
src ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ └───┘ ┴┴┴ ┴┴ ┴ ┴┴ ┴ ┴
doc ┴ └───┘ ┴
94 begin
st └─────
95 rw [nhds_eq_comap_uniformity, filter.comap_comap_comp],
id └──────────────────────┘ └─────────────────────┘
src └──┘└──────────────────────┘└┘└─────────────────────┘┴
typ └──┘└──────────────────────┘└┘└─────────────────────┘┴
doc └──┘ └┘ ┴
txt └──┘ └┘ ┴
par └──┘ └┘ ┴
pid └┘ └┘ ┴
st ─────────────────────────────┘└───────────────────────┘└──
96 refine le_antisymm (filter.map_le_iff_le_comap.1 _) _,
id └─────────┘ └────────────────────────┘
src └─────┘└─────────┘┴ └────────────────────────┘└─────┘
typ └─────┘└─────────┘┴ └────────────────────────┘└─────┘
doc └─────┘ ┴ └─────┘
txt └─────┘ ┴ └─────┘
par └─────┘ ┴ └─────┘
pid ┴ ┴ └─────┘
st ──────────────────────────────────────────────────────┘└─
97 { assume s hs,
src └─────────┘
typ └─────────┘
doc └─────────┘
txt └─────────┘
par └─────────┘
pid └─────────┘
st ───┘└─────────┘└─
98 rcases mem_uniformity_of_uniform_continuous_invariant uniform_continuous_sub hs with ⟨t, ht, hts⟩,
id └────────────────────────────────────────────┘ └────────────────────┘ └┘
src └─────┘└────────────────────────────────────────────┘┴└────────────────────┘┴ └────────────────┘
typ └─────┘└────────────────────────────────────────────┘┴└────────────────────┘┴└┘└────────────────┘
doc └─────┘ ┴ ┴ └────────────────┘
txt └─────┘ ┴ ┴ └────────────────┘
par └─────┘ ┴ ┴ └────────────────┘
pid ┴ ┴ ┴ └────────────────┘
st ────────────────────────────────────────────────────────────────────────────────────────────────────┘└─
99 refine mem_map.2 (mem_sets_of_superset ht _),
id └─────┘ └──────────────────┘ └┘
src └─────┘└─────┘└─┘ └──────────────────┘┴ └─┘
typ └─────┘└─────┘└─┘ └──────────────────┘┴└┘└─┘
doc └─────┘ └─┘ ┴ └─┘
txt └─────┘ └─┘ ┴ └─┘
par └─────┘ └─┘ ┴ └─┘
pid ┴ └─┘ ┴ └─┘
st ───────────────────────────────────────────────┘└─
100 rintros ⟨a, b⟩,
src └────────────┘
typ └────────────┘
doc └────────────┘
txt └────────────┘
par └────────────┘
pid └─────┘
st ─────────────────┘└─
101 simpa [subset_def] using hts a b a },
id └────────┘ └─┘ ┴ ┴
src └─────┘└────────┘└──────┘ ┴ ┴ ┴ ┴
typ └─────┘└────────┘└──────┘└─┘┴ ┴┴┴┴┴
doc └─────┘ └──────┘ ┴ ┴ ┴ ┴
txt └─────┘ └──────┘ ┴ ┴ ┴ ┴
par └─────┘ └──────┘ ┴ ┴ ┴ ┴
pid ┴┴ ┴┴└────┘ ┴ ┴ ┴ ┴
st ──────────────────────────────────────┘└┘└
102 { assume s hs,
src └─────────┘
typ └─────────┘
doc └─────────┘
txt └─────────┘
par └─────────┘
pid └─────────┘
st ──────────────┘└─
103 rcases mem_uniformity_of_uniform_continuous_invariant uniform_continuous_add hs with ⟨t, ht, hts⟩,
id └────────────────────────────────────────────┘ └────────────────────┘ └┘
src └─────┘└────────────────────────────────────────────┘┴└────────────────────┘┴ └────────────────┘
typ └─────┘└────────────────────────────────────────────┘┴└────────────────────┘┴└┘└────────────────┘
doc └─────┘ ┴ ┴ └────────────────┘
txt └─────┘ ┴ ┴ └────────────────┘
par └─────┘ ┴ ┴ └────────────────┘
pid ┴ ┴ ┴ └────────────────┘
st ────────────────────────────────────────────────────────────────────────────────────────────────────┘└─
104 refine ⟨_, ht, _⟩,
id └┘
src └─────┘ └─┘ └──┘
typ └─────┘ └─┘└┘└──┘
doc └─────┘ └─┘ └──┘
txt └─────┘ └─┘ └──┘
par └─────┘ └─┘ └──┘
pid ┴ └─┘ └──┘
st ────────────────────┘└─
105 rintros ⟨a, b⟩, simpa [subset_def] using hts 0 (b - a) a }
id └────────┘ └─┘ ┴ ┴ ┴
src └────────────┘ └─────┘└────────┘└──────┘ └─┘ ┴┴┴ └┘ ┴
typ └────────────┘ └─────┘└────────┘└──────┘└─┘└─┘ ┴┴┴┴ └┘┴┴
doc └────────────┘ └─────┘ └──────┘ └─┘ ┴ ┴ └┘ ┴
txt └────────────┘ └─────┘ └──────┘ └─┘ ┴ ┴ └┘ ┴
par └────────────┘ └─────┘ └──────┘ └─┘ ┴ ┴ └┘ ┴
pid └─────┘ ┴┴ ┴┴└────┘ └─┘ ┴ ┴ └┘ ┴
st ─────────────────┘└─────────────────────────────────────────┘└─
106 end
st ──┘
107 end
108
109 lemma group_separation_rel (x y : α) : (x, y) ∈ separation_rel α ↔ x - y ∈ closure ({0} : set α) :=
id ┴ ┴┴ ┴ ┴ └────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ └─┘ ┴
src ┴ ┴ └────────────┘ ┴ ┴ ┴ └─────┘ ┴ └─┘
typ ┴ ┴┴ ┴ ┴ └────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ └─┘ ┴
doc └────────────┘ └─────┘
110 have embedding (λa, a + (y - x)), from (uniform_embedding_translate (y - x)).embedding,
id └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─────────────────────────┘ ┴ ┴ ┴ └───────┘
src └───────┘ ┴ ┴ └─────────────────────────┘ ┴ └───────┘
typ └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─────────────────────────┘ ┴ ┴ ┴ └───────┘
doc └───────┘
111 show (x, y) ∈ ⋂₀ (𝓤 α).sets ↔ x - y ∈ closure ({0} : set α),
id ┴┴ ┴ ┴ └┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ └─┘ ┴
src ┴ ┴ └┘ ┴ └──┘ ┴ ┴ ┴ └─────┘ ┴ └─┘
typ ┴┴ ┴ ┴ └┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ └─┘ ┴
doc └┘ ┴ └─────┘
112 begin
st └─────
113 rw [this.closure_eq_preimage_closure_image, uniformity_eq_comap_nhds_zero α, sInter_comap_sets],
id └───────────────────────────┘ ┴ └───────────────┘
src └──┘ └┘└───────────────────────────┘┴ └┘└───────────────┘┴
typ └──┘└────────────────────────────────────┘└┘└───────────────────────────┘┴┴└┘└───────────────┘┴
doc └──┘ └┘ ┴ └┘ ┴
txt └──┘ └┘ ┴ └┘ ┴
par └──┘ └┘ ┴ └┘ ┴
pid └┘ └┘ ┴ └┘ ┴
st ───────────────────────────────────────────┘└───────────────────────────────┘└─────────────────┘└──
114 simp [mem_closure_iff_nhds, inter_singleton_nonempty]
id └──────────────────┘ └──────────────────────┘
src └────┘└──────────────────┘└┘└──────────────────────┘└┘
typ └────┘└──────────────────┘└┘└──────────────────────┘└┘
doc └────┘ └┘ └┘
txt └────┘ └┘ └┘
par └────┘ └┘ └┘
pid ┴┴ └┘ ┴┴
st ───────────────────────────────────────────────────────┘
115 end
st └─┘
116
117 lemma uniform_continuous_of_tendsto_zero [uniform_space β] [add_group β] [uniform_add_group β]
id └───────────┘ ┴ └───────┘ ┴ └───────────────┘ ┴
src └───────────┘ └───────┘ └───────────────┘
typ └───────────┘ ┴ └───────┘ ┴ └───────────────┘ ┴
doc └───────────┘ └───────────────┘
118 {f : α → β} [is_add_group_hom f] (h : tendsto f (𝓝 0) (𝓝 0)) :
id ┴ ┴ └──────────────┘ ┴ └─────┘ ┴ ┴ ┴
src └──────────────┘ └─────┘ ┴ ┴
typ ┴ ┴ └──────────────┘ ┴ └─────┘ ┴ ┴ ┴
doc └──────────────┘ └─────┘ ┴ ┴
119 uniform_continuous f :=
id └────────────────┘ ┴
src └────────────────┘
typ └────────────────┘ ┴
120 begin
st └─────
121 have : ((λx:β×β, x.2 - x.1) ∘ (λx:α×α, (f x.1, f x.2))) = (λx:α×α, f (x.2 - x.1)),
id ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─────┘ └┘ ┴ └┘ └─┘┴┴ └──┘┴┴ └┘ └┘┴ ┴ └──┘ ┴ └────┘┴┴ └┘ └┘ ┴ └─┘ ┴ └──┘
typ └─────┘ └┘ ┴┴└┘ └─┘┴┴ └──┘┴┴ └┘ ┴ └┘┴ ┴ └──┘ ┴ └────┘┴┴ └┘ ┴└┘┴┴ └─┘ ┴ └──┘
doc └─────┘ └┘ └┘ └─┘ ┴ └──┘ ┴ └┘ └┘ ┴ └──┘ ┴ └────┘ ┴ └┘ └┘ ┴ └─┘ ┴ └──┘
txt └─────┘ └┘ └┘ └─┘ ┴ └──┘ ┴ └┘ └┘ ┴ └──┘ ┴ └────┘ ┴ └┘ └┘ ┴ └─┘ ┴ └──┘
par └─────┘ └┘ └┘ └─┘ ┴ └──┘ ┴ └┘ └┘ ┴ └──┘ ┴ └────┘ ┴ └┘ └┘ ┴ └─┘ ┴ └──┘
pid └───┘└┘ └┘ └┘ └─┘ ┴ └──┘ ┴ └┘ └┘ ┴ └──┘ ┴ └────┘ ┴ └┘ └┘ ┴ └─┘ ┴ └──┘
st ──────────────────────────────────────────────────────────────────────────────────┘└─
122 { simp only [is_add_group_hom.map_sub f] },
id └──────────────────────┘ ┴
src └─────────┘└──────────────────────┘┴ └┘
typ └─────────┘└──────────────────────┘┴┴└┘
doc └─────────┘└──────────────────────┘┴ └┘
txt └─────────┘ ┴ └┘
par └─────────┘ ┴ └┘
pid ┴└──┘└┘ ┴ ┴┴
st ───┘└─────────────────────────────────────┘└┘└
123 rw [uniform_continuous, uniformity_eq_comap_nhds_zero α, uniformity_eq_comap_nhds_zero β,
id └────────────────┘ └───────────────────────────┘ ┴ └───────────────────────────┘ ┴
src └──┘└────────────────┘└┘└───────────────────────────┘┴ └┘└───────────────────────────┘┴ └─
typ └──┘└────────────────┘└┘└───────────────────────────┘┴┴└┘└───────────────────────────┘┴┴└─
doc └──┘ └┘ ┴ └┘ ┴ └─
txt └──┘ └┘ ┴ └┘ ┴ └─
par └──┘ └┘ ┴ └┘ ┴ └─
pid └┘ └┘ ┴ └┘ ┴ └─
st ───────────────────────┘└───────────────────────────────┘└───────────────────────────────┘└─
124 tendsto_comap_iff, this],
id └───────────────┘ └──┘
src ───┘└───────────────┘└┘ ┴
typ ───┘└───────────────┘└┘└──┘┴
doc ───┘ └┘ ┴
txt ───┘ └┘ ┴
par ───┘ └┘ ┴
pid ───┘ └┘ ┴
st ────────────────────┘└────┘└──
125 exact tendsto.comp h tendsto_comap
id └──────────┘ ┴ └───────────┘
src └────┘└──────────┘┴ ┴└───────────┘┴
typ └────┘└──────────┘┴┴┴└───────────┘┴
doc └────┘ ┴ ┴ ┴
txt └────┘ ┴ ┴ ┴
par └────┘ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴
st ────────────────────────────────────┘
126 end
st └─┘
127
128 lemma uniform_continuous_of_continuous [uniform_space β] [add_group β] [uniform_add_group β]
id └───────────┘ ┴ └───────┘ ┴ └───────────────┘ ┴
src └───────────┘ └───────┘ └───────────────┘
typ └───────────┘ ┴ └───────┘ ┴ └───────────────┘ ┴
doc └───────────┘ └───────────────┘
129 {f : α → β} [is_add_group_hom f] (h : continuous f) :
id ┴ ┴ └──────────────┘ ┴ └────────┘ ┴
src └──────────────┘ └────────┘
typ ┴ ┴ └──────────────┘ ┴ └────────┘ ┴
doc └──────────────┘ └────────┘
130 uniform_continuous f :=
id └────────────────┘ ┴
src └────────────────┘
typ └────────────────┘ ┴
131 uniform_continuous_of_tendsto_zero $
id └────────────────────────────────┘
src └────────────────────────────────┘
typ └────────────────────────────────┘
132 suffices tendsto f (𝓝 0) (𝓝 (f 0)), by rwa [is_add_group_hom.map_zero f] at this,
id └─────┘ ┴ ┴ ┴ ┴ └───────────────────────┘ ┴
src └─────┘ ┴ ┴ └───┘└───────────────────────┘┴ └───────┘
typ └─────┘ ┴ ┴ ┴ ┴ └───┘└───────────────────────┘┴┴└───────┘
doc └─────┘ ┴ ┴ └───┘ ┴ └───────┘
txt └───┘ ┴ └───────┘
par └───┘ ┴ └───────┘
pid └┘ ┴ ┴└──────┘
st └───────────────────────────────┘┴└──────┘
133 h.tendsto 0
id ┴└──────┘
src └──────┘
typ ┴└──────┘
134
135 end uniform_add_group
136
137 section topological_add_comm_group
138 universes u v w x
139 open filter
140
141 variables {G : Type u} [add_comm_group G] [topological_space G] [topological_add_group G]
id └────────────┘ └───────────────┘ └───────────────────┘
src └────────────┘ └───────────────┘ └───────────────────┘
typ └────────────┘ └───────────────┘ └───────────────────┘
doc └───────────────┘ └───────────────────┘
142
143 variable (G)
144 def topological_add_group.to_uniform_space : uniform_space G :=
id └───────────┘ ┴
src └───────────┘
typ └───────────┘ ┴
doc └───────────┘
145 { uniformity := comap (λp:G×G, p.2 - p.1) (𝓝 0),
id └───┘ ┴┴┴ ┴┴ ┴ ┴┴ ┴
src └───┘ ┴ ┴ ┴ ┴ ┴
typ └───┘ ┴┴┴ ┴┴ ┴ ┴┴ ┴
doc └───┘ ┴
146 refl :=
147 by refine map_le_iff_le_comap.1 (le_trans _ (pure_le_nhds 0));
id └─────────────────┘ └──────┘ └──────────┘
src └─────┘└─────────────────┘└─┘ └──────┘└─┘ └──────────┘└──┘
typ └─────┘└─────────────────┘└─┘ └──────┘└─┘ └──────────┘└──┘
doc └─────┘ └─┘ └─┘ └──┘
txt └─────┘ └─┘ └─┘ └──┘
par └─────┘ └─┘ └─┘ └──┘
pid ┴ └─┘ └─┘ └──┘
st └────────────────────────────────────────────────────────────
148 simp [set.subset_def] {contextual := tt},
id └────────────┘ └┘
src └────┘└────────────┘└┘ └────────────┘└┘┴
typ └────┘└────────────┘└┘ └────────────┘└┘┴
doc └────┘ └┘ └────────────┘ ┴
txt └────┘ └┘ └────────────┘ ┴
par └────┘ └┘ └────────────┘ ┴
pid ┴┴ ┴┴ └────────────┘ ┴
st ─────────────────────────────────────────────┘
149 symm :=
150 begin
st └─────
151 suffices : tendsto ((λp, -p) ∘ (λp:G×G, p.2 - p.1)) (comap (λp:G×G, p.2 - p.1) (𝓝 0)) (𝓝 (-0)),
id └─────┘ ┴ ┴ ┴ ┴ └───┘ ┴ ┴
src └─────────┘└─────┘┴ └─┘┴ └┘┴┴ └┘ ┴ └┘ └─┘┴┴ └───┘ └───┘┴ └┘ └┘ └─┘ ┴ └──┘ ┴└───┘ ┴ └─┘
typ └─────────┘└─────┘┴ └─┘┴ └┘┴┴ └┘ ┴ └┘ └─┘┴┴ └───┘ └───┘┴ └┘ ┴└┘ └─┘ ┴ └──┘ ┴└───┘ ┴ └─┘
doc └─────────┘└─────┘┴ └─┘ └┘ ┴ └┘ └┘ └─┘ ┴ └───┘ └───┘┴ └┘ └┘ └─┘ ┴ └──┘ ┴└───┘ ┴ └─┘
txt └─────────┘ ┴ └─┘ └┘ ┴ └┘ └┘ └─┘ ┴ └───┘ ┴ └┘ └┘ └─┘ ┴ └──┘ └───┘ ┴ └─┘
par └─────────┘ ┴ └─┘ └┘ ┴ └┘ └┘ └─┘ ┴ └───┘ ┴ └┘ └┘ └─┘ ┴ └──┘ └───┘ ┴ └─┘
pid └───────┘└┘ ┴ └─┘ └┘ ┴ └┘ └┘ └─┘ ┴ └───┘ ┴ └┘ └┘ └─┘ ┴ └──┘ └───┘ ┴ └─┘
st ─────────────────────────────────────────────────────────────────────────────────────────────────┘└─
152 { simpa [(∘), tendsto_comap_iff] },
id ┴ └───────────────┘
src └─────┘┴└──┘└───────────────┘└┘
typ └─────┘┴└──┘└───────────────┘└┘
doc └─────┘ └──┘ └┘
txt └─────┘ └──┘ └┘
par └─────┘ └──┘ └┘
pid ┴┴ └──┘ ┴┴
st ─────┘└─────────────────────────────┘└┘└
153 exact tendsto.comp (tendsto.neg tendsto_id) tendsto_comap
id └──────────┘ └─────────┘ └────────┘ └───────────┘
src └────┘└──────────┘┴ └─────────┘┴└────────┘└┘└───────────┘└
typ └────┘└──────────┘┴ └─────────┘┴└────────┘└┘└───────────┘└
doc └────┘ ┴ ┴ └┘ └
txt └────┘ ┴ ┴ └┘ └
par └────┘ ┴ ┴ └┘ └
pid ┴ ┴ ┴ └┘ └
st ──────────────────────────────────────────────────────────────
154 end,
src ─┘
typ ─┘
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘└─┘
155 comp :=
156 begin
st └─────
157 intros D H,
src └────────┘
typ └────────┘
doc └────────┘
txt └────────┘
par └────────┘
pid └──┘
st ─────────────┘└─
158 rw mem_lift'_sets,
id └────────────┘
src └─┘└────────────┘
typ └─┘└────────────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ────────────────────┘└─
159 { rcases H with ⟨U, U_nhds, U_sub⟩,
id ┴
src └─────┘ └──────────────────────┘
typ └─────┘┴└──────────────────────┘
doc └─────┘ └──────────────────────┘
txt └─────┘ └──────────────────────┘
par └─────┘ └──────────────────────┘
pid ┴ └──────────────────────┘
st ─────┘└──────────────────────────────┘└─
160 rcases exists_nhds_half U_nhds with ⟨V, ⟨V_nhds, V_sum⟩⟩,
id └──────────────┘ └────┘
src └─────┘└──────────────┘┴ └────────────────────────┘
typ └─────┘└──────────────┘┴└────┘└────────────────────────┘
doc └─────┘ ┴ └────────────────────────┘
txt └─────┘ ┴ └────────────────────────┘
par └─────┘ ┴ └────────────────────────┘
pid ┴ ┴ └────────────────────────┘
st ─────────────────────────────────────────────────────────────┘└─
161 existsi ((λp:G×G, p.2 - p.1) ⁻¹' V),
id ┴ └─┘ ┴
src └──────┘ └┘ └┘ └─┘ ┴ └──┘└─┘┴ ┴
typ └──────┘ └┘ ┴└┘ └─┘ ┴ └──┘└─┘┴┴┴
doc └──────┘ └┘ └┘ └─┘ ┴ └──┘└─┘┴ ┴
txt └──────┘ └┘ └┘ └─┘ ┴ └──┘ ┴ ┴
par └──────┘ └┘ └┘ └─┘ ┴ └──┘ ┴ ┴
pid ┴ └┘ └┘ └─┘ ┴ └──┘ ┴ ┴
st ────────────────────────────────────────┘└─
162 have H : (λp:G×G, p.2 - p.1) ⁻¹' V ∈ comap (λp:G×G, p.2 - p.1) (𝓝 (0 : G)),
id ┴ ┴ └───┘ ┴
src └───────┘ └┘ └┘ └─┘ ┴ └──┘ ┴ ┴┴┴└───┘┴ └┘ └┘ └─┘ ┴ └──┘ ┴ └──┘ └┘
typ └───────┘ └┘ └┘ └─┘ ┴ └──┘ ┴┴┴┴┴└───┘┴ └┘ └┘ └─┘ ┴ └──┘ ┴ └──┘┴└┘
doc └───────┘ └┘ └┘ └─┘ ┴ └──┘ ┴ ┴ ┴└───┘┴ └┘ └┘ └─┘ ┴ └──┘ ┴ └──┘ └┘
txt └───────┘ └┘ └┘ └─┘ ┴ └──┘ ┴ ┴ ┴ ┴ └┘ └┘ └─┘ ┴ └──┘ ┴ └──┘ └┘
par └───────┘ └┘ └┘ └─┘ ┴ └──┘ ┴ ┴ ┴ ┴ └┘ └┘ └─┘ ┴ └──┘ ┴ └──┘ └┘
pid └────┘└─┘ └┘ └┘ └─┘ ┴ └──┘ ┴ ┴ ┴ ┴ └┘ └┘ └─┘ ┴ └──┘ ┴ └──┘ └┘
st ───────────────────────────────────────────────────────────────────────────────┘
163 by existsi [V, V_nhds] ; refl,
id ┴ └────┘
src └───────┘ └┘ └┘ └──┘
typ └───────┘┴└┘└────┘└┘ └──┘
doc └───────┘ └┘ └┘ └──┘
txt └───────┘ └┘ └┘ └──┘
par └───────┘ └┘ └┘ └──┘
pid └┘ └┘ ┴┴
st └─
164 existsi H,
id ┴
src └──────┘
typ └──────┘┴
doc └──────┘
txt └──────┘
par └──────┘
pid ┴
st ──────────────┘└─
165 have comp_rel_sub : comp_rel ((λp:G×G, p.2 - p.1) ⁻¹' V) ((λp:G×G, p.2 - p.1) ⁻¹' V) ⊆ (λp:G×G, p.2 - p.1) ⁻¹' U,
id └──────┘ ┴ ┴ ┴ ┴
src └──────────────────┘└──────┘┴ └┘ └┘ └─┘ ┴ └──┘ ┴ └┘ └┘ └┘ └─┘ ┴ └──┘ ┴ └┘┴┴ └┘ └┘ └─┘ ┴ └──┘ ┴
typ └──────────────────┘└──────┘┴ └┘ └┘ └─┘ ┴ └──┘ ┴ └┘ └┘ └┘ └─┘ ┴ └──┘ ┴┴└┘┴┴ └┘ ┴└┘ └─┘ ┴ └──┘ ┴┴
doc └──────────────────┘└──────┘┴ └┘ └┘ └─┘ ┴ └──┘ ┴ └┘ └┘ └┘ └─┘ ┴ └──┘ ┴ └┘ ┴ └┘ └┘ └─┘ ┴ └──┘ ┴
txt └──────────────────┘ ┴ └┘ └┘ └─┘ ┴ └──┘ ┴ └┘ └┘ └┘ └─┘ ┴ └──┘ ┴ └┘ ┴ └┘ └┘ └─┘ ┴ └──┘ ┴
par └──────────────────┘ ┴ └┘ └┘ └─┘ ┴ └──┘ ┴ └┘ └┘ └┘ └─┘ ┴ └──┘ ┴ └┘ ┴ └┘ └┘ └─┘ ┴ └──┘ ┴
pid └───────────────┘└─┘ ┴ └┘ └┘ └─┘ ┴ └──┘ ┴ └┘ └┘ └┘ └─┘ ┴ └──┘ ┴ └┘ ┴ └┘ └┘ └─┘ ┴ └──┘ ┴
st ─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘└─
166 begin
st ──────────┘└
167 intros p p_comp_rel,
src └─────────────────┘
typ └─────────────────┘
doc └─────────────────┘
txt └─────────────────┘
par └─────────────────┘
pid └───────────┘
st ──────────────────────────┘└─
168 rcases p_comp_rel with ⟨z, ⟨Hz1, Hz2⟩⟩,
id └────────┘
src └─────┘ └───────────────────┘
typ └─────┘└────────┘└───────────────────┘
doc └─────┘ └───────────────────┘
txt └─────┘ └───────────────────┘
par └─────┘ └───────────────────┘
pid ┴ └───────────────────┘
st ─────────────────────────────────────────────┘└─
169 simpa using V_sum _ _ Hz1 Hz2
id └───┘ └─┘ └─┘
src └──────────┘ └───┘ ┴ └
typ └──────────┘└───┘└───┘└─┘┴└─┘└
doc └──────────┘ └───┘ ┴ └
txt └──────────┘ └───┘ ┴ └
par └──────────┘ └───┘ ┴ └
pid ┴└────┘ └───┘ ┴ └
st ──────────────────────────────────────
170 end,
src ─────┘
typ ─────┘
doc ─────┘
txt ─────┘
par ─────┘
pid ─────┘
st ─────┘└─┘└─
171 exact set.subset.trans comp_rel_sub U_sub },
id └──────────────┘ └──────────┘ └───┘
src └────┘└──────────────┘┴ ┴ ┴
typ └────┘└──────────────┘┴└──────────┘┴└───┘┴
doc └────┘ ┴ ┴ ┴
txt └────┘ ┴ ┴ ┴
par └────┘ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴
st ───────────────────────────────────────────────┘└┘└
172 { exact monotone_comp_rel monotone_id monotone_id }
id └───────────────┘ └─────────┘
src └────┘└───────────────┘┴ ┴└─────────┘┴
typ └────┘└───────────────┘┴ ┴└─────────┘┴
doc └────┘ ┴ ┴ ┴
txt └────┘ ┴ ┴ ┴
par └────┘ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴
st ─────────────────────────────────────────────────────┘└─
173 end,
st ────┘
174 is_open_uniformity :=
175 begin
st └─────
176 intro S,
src └─────┘
typ └─────┘
doc └─────┘
txt └─────┘
par └─────┘
pid └┘
st ──────────┘└─
177 let S' := λ x, {p : G × G | p.1 = x → p.2 ∈ S},
id ┴ ┴ ┴ ┴
src └────────┘ └──┘┴└──┘ ┴ ┴ └─┘ └─┘┴┴ ┴ ┴ └─┘ ┴ ┴
typ └────────┘ └──┘┴└──┘ ┴ ┴┴└─┘ └─┘┴┴ ┴ ┴ └─┘ ┴┴┴
doc └────────┘ └──┘ └──┘ ┴ ┴ └─┘ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴
txt └────────┘ └──┘ └──┘ ┴ ┴ └─┘ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴
par └────────┘ └──┘ └──┘ ┴ ┴ └─┘ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴
pid └────┘┴└─┘ └──┘ └──┘ ┴ ┴ └─┘ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴
st ─────────────────────────────────────────────────┘└─
178 show is_open S ↔ ∀ (x : G), x ∈ S → S' x ∈ comap (λp:G×G, p.2 - p.1) (𝓝 (0 : G)),
id └─────┘ ┴ ┴ └┘ └───┘ ┴
src └───┘└─────┘┴ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴└───┘┴ └┘ └┘ └─┘ ┴ └──┘ ┴ └──┘ └┘
typ └───┘└─────┘┴ ┴ ┴ └────┘ ┴ ┴ ┴┴┴┴┴ ┴└┘┴ ┴ ┴└───┘┴ └┘ └┘ └─┘ ┴ └──┘ ┴ └──┘┴└┘
doc └───┘└─────┘┴ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴└───┘┴ └┘ └┘ └─┘ ┴ └──┘ ┴ └──┘ └┘
txt └───┘ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └┘ └─┘ ┴ └──┘ ┴ └──┘ └┘
par └───┘ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └┘ └─┘ ┴ └──┘ ┴ └──┘ └┘
pid └───┘ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └┘ └─┘ ┴ └──┘ ┴ └──┘ └┘
st ───────────────────────────────────────────────────────────────────────────────────┘└─
179 rw [is_open_iff_mem_nhds],
id └──────────────────┘
src └──┘└──────────────────┘┴
typ └──┘└──────────────────┘┴
doc └──┘ ┴
txt └──┘ ┴
par └──┘ ┴
pid └┘ ┴
st ───────────────────────────┘└──
180 refine forall_congr (assume a, forall_congr (assume ha, _)),
id └──────────┘
src └─────┘ ┴ └──┘└──────────┘┴ └──────┘
typ └─────┘ ┴ └──┘└──────────┘┴ └──────┘
doc └─────┘ ┴ └──┘ ┴ └──────┘
txt └─────┘ ┴ └──┘ ┴ └──────┘
par └─────┘ ┴ └──┘ ┴ └──────┘
pid ┴ ┴ └──┘ ┴ └──────┘
st ──────────────────────────────────────────────────────────────┘└─
181 rw [← nhds_translation a, mem_comap_sets, mem_comap_sets],
id └──────────────┘ ┴ └────────────┘ └────────────┘
src └────┘└──────────────┘┴ └┘└────────────┘└┘└────────────┘┴
typ └────┘└──────────────┘┴┴└┘└────────────┘└┘└────────────┘┴
doc └────┘ ┴ └┘ └┘ ┴
txt └────┘ ┴ └┘ └┘ ┴
par └────┘ ┴ └┘ └┘ ┴
pid └──┘ ┴ └┘ └┘ ┴
st ───────────────────────────┘└──────────────┘└──────────────┘└──
182 refine exists_congr (assume t, exists_congr (assume ht, _)),
id └──────────┘
src └─────┘ ┴ └──┘└──────────┘┴ └──────┘
typ └─────┘ ┴ └──┘└──────────┘┴ └──────┘
doc └─────┘ ┴ └──┘ ┴ └──────┘
txt └─────┘ ┴ └──┘ ┴ └──────┘
par └─────┘ ┴ └──┘ ┴ └──────┘
pid ┴ ┴ └──┘ ┴ └──────┘
st ──────────────────────────────────────────────────────────────┘└─
183 show (λ (y : G), y - a) ⁻¹' t ⊆ S ↔ (λ (p : G × G), p.snd - p.fst) ⁻¹' t ⊆ S' a,
id ┴ ┴ └──┘ └──┘ ┴ └┘ ┴
src └───┘ └────┘ └─┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └────┘ ┴ ┴ └─┘ └──┘┴ ┴ └──┘└┘ ┴ ┴ ┴ ┴
typ └───┘ └────┘ └─┘ ┴ ┴ └┘ ┴ ┴ ┴┴┴ ┴ └────┘ ┴ ┴┴└─┘ └──┘┴ ┴ └──┘└┘ ┴┴┴ ┴└┘┴┴
doc └───┘ └────┘ └─┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └────┘ ┴ ┴ └─┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴
txt └───┘ └────┘ └─┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └────┘ ┴ ┴ └─┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴
par └───┘ └────┘ └─┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └────┘ ┴ ┴ └─┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴
pid └───┘ └────┘ └─┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └────┘ ┴ ┴ └─┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴
st ─────────────────────────────────────────────────────────────────────────────────────
184 split,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
st ────────┘└─
185 { rintros h ⟨x, y⟩ hx rfl, exact h hx },
id ┴ └┘
src └─────────────────────┘ └────┘ ┴ ┴
typ └─────────────────────┘ └────┘┴┴└┘┴
doc └─────────────────────┘ └────┘ ┴ ┴
txt └─────────────────────┘ └────┘ ┴ ┴
par └─────────────────────┘ └────┘ ┴ ┴
pid └──────────────┘ ┴ ┴ ┴
st ─────┘└─────────────────────┘└───────────┘└┘└
186 { rintros h x hx, exact @h (a, x) hx rfl }
id ┴ ┴ ┴ └┘ └─┘
src └────────────┘ └────┘ ┴ └┘ └┘ ┴└─┘┴
typ └────────────┘ └────┘ ┴┴ ┴└┘┴└┘└┘┴└─┘┴
doc └────────────┘ └────┘ ┴ └┘ └┘ ┴ ┴
txt └────────────┘ └────┘ ┴ └┘ └┘ ┴ ┴
par └────────────┘ └────┘ ┴ └┘ └┘ ┴ ┴
pid └─────┘ ┴ ┴ └┘ └┘ ┴ ┴
st ───────────────────┘└───────────────────────┘└─
187 end }
st ────┘
188
189 section
190 local attribute [instance] topological_add_group.to_uniform_space
id └────────────────────────────────────┘
src └────────────────────────────────────┘
typ └────────────────────────────────────┘
191
192 lemma uniformity_eq_comap_nhds_zero' : 𝓤 G = comap (λp:G×G, p.2 - p.1) (𝓝 (0 : G)) := rfl
id ┴ ┴ ┴ └───┘ ┴┴┴ ┴┴ ┴ ┴┴ ┴ ┴ └─┘
src ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ └─┘
typ ┴ ┴ ┴ └───┘ ┴┴┴ ┴┴ ┴ ┴┴ ┴ ┴ └─┘
doc ┴ └───┘ ┴
193
194 variable {G}
195 lemma topological_add_group_is_uniform : uniform_add_group G :=
id └───────────────┘ ┴
src └───────────────┘
typ └───────────────┘ ┴
doc └───────────────┘
196 have tendsto
id └─────┘
src └─────┘
typ └─────┘
doc └─────┘
197 ((λp:(G×G), p.1 - p.2) ∘ (λp:(G×G)×(G×G), (p.1.2 - p.1.1, p.2.2 - p.2.1)))
id ┴┴┴ ┴┴ ┴ ┴┴ ┴ ┴┴┴ ┴ ┴┴┴ ┴┴┴ ┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴ ┴┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴┴┴ ┴┴ ┴ ┴┴ ┴ ┴┴┴ ┴ ┴┴┴ ┴┴┴ ┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴ ┴┴ ┴
198 (comap (λp:(G×G)×(G×G), (p.1.2 - p.1.1, p.2.2 - p.2.1)) ((𝓝 0).prod (𝓝 0)))
id └───┘ ┴┴┴ ┴ ┴┴┴ ┴┴┴ ┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴ ┴┴ ┴ ┴ └──┘ ┴
src └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴
typ └───┘ ┴┴┴ ┴ ┴┴┴ ┴┴┴ ┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴ ┴┴ ┴ ┴ └──┘ ┴
doc └───┘ ┴ └──┘ ┴
199 (𝓝 (0 - 0)) :=
id ┴ ┴
src ┴ ┴
typ ┴ ┴
doc ┴
200 (tendsto_fst.sub tendsto_snd).comp tendsto_comap,
id └─────────┘└──┘ └─────────┘ └──┘ └───────────┘
src └─────────┘└──┘ └─────────┘ └──┘ └───────────┘
typ └─────────┘└──┘ └─────────┘ └──┘ └───────────┘
201 begin
st └─────
202 constructor,
src └─────────┘
typ └─────────┘
doc └─────────┘
txt └─────────┘
par └─────────┘
st ────────────┘└─
203 rw [uniform_continuous, uniformity_prod_eq_prod, tendsto_map'_iff,
id └────────────────┘ └─────────────────────┘ └──────────────┘
src └──┘└────────────────┘└┘└─────────────────────┘└┘└──────────────┘└─
typ └──┘└────────────────┘└┘└─────────────────────┘└┘└──────────────┘└─
doc └──┘ └┘ └┘ └─
txt └──┘ └┘ └┘ └─
par └──┘ └┘ └┘ └─
pid └┘ └┘ └┘ └─
st ───────────────────────┘└───────────────────────┘└────────────────┘└─
204 uniformity_eq_comap_nhds_zero' G, tendsto_comap_iff, prod_comap_comap_eq],
id ┴ └───────────────┘ └─────────────────┘
src ───┘ ┴ └┘└───────────────┘└┘└─────────────────┘┴
typ ───┘ ┴┴└┘└───────────────┘└┘└─────────────────┘┴
doc ───┘ ┴ └┘ └┘ ┴
txt ───┘ ┴ └┘ └┘ ┴
par ───┘ ┴ └┘ └┘ ┴
pid ───┘ ┴ └┘ └┘ ┴
st ───────────────────────────────────┘└─────────────────┘└───────────────────┘└──
205 simpa [(∘)]
id ┴
src └─────┘┴└──┘
typ └─────┘┴└──┘
doc └─────┘ └──┘
txt └─────┘ └──┘
par └─────┘ └──┘
pid ┴┴ └─┘┴
st ─────────────┘
206 end
st └─┘
207 end
208
209 lemma to_uniform_space_eq {α : Type*} [u : uniform_space α] [add_comm_group α] [uniform_add_group α]:
id └───────────┘ ┴ └────────────┘ ┴ └───────────────┘ ┴
src └───────────┘ └────────────┘ └───────────────┘
typ └───────────┘ ┴ └────────────┘ ┴ └───────────────┘ ┴
doc └───────────┘ └───────────────┘
210 topological_add_group.to_uniform_space α = u :=
id └────────────────────────────────────┘ ┴ ┴ ┴
src └────────────────────────────────────┘ ┴
typ └────────────────────────────────────┘ ┴ ┴ ┴
211 begin
st └─────
212 ext : 1,
src └─────┘
typ └─────┘
doc └─────┘
txt └─────┘
par └─────┘
pid ┴└┘┴
st ────────┘└─
213 show @uniformity α (topological_add_group.to_uniform_space α) = 𝓤 α,
id └────────┘ ┴ ┴
src └───┘ └────────┘┴ ┴ ┴ └┘┴┴ ┴
typ └───┘ └────────┘┴ ┴ ┴ └┘┴┴ ┴┴
doc └───┘ └────────┘┴ ┴ ┴ └┘ ┴ ┴
txt └───┘ ┴ ┴ ┴ └┘ ┴ ┴
par └───┘ ┴ ┴ ┴ └┘ ┴ ┴
pid └───┘ ┴ ┴ ┴ └┘ ┴ ┴
st ────────────────────────────────────────────────────────────────────┘└─
214 rw [uniformity_eq_comap_nhds_zero' α, uniformity_eq_comap_nhds_zero α]
id ┴ └───────────────────────────┘ ┴
src └──┘ ┴ └┘└───────────────────────────┘┴ └┘
typ └──┘ ┴┴└┘└───────────────────────────┘┴┴└┘
doc └──┘ ┴ └┘ ┴ └┘
txt └──┘ ┴ └┘ ┴ └┘
par └──┘ ┴ └┘ ┴ └┘
pid └┘ ┴ └┘ ┴ ┴┴
st ─────────────────────────────────────┘└───────────────────────────────┘┴┴
215 end
st └─┘
216
217 end topological_add_comm_group
218
219 namespace add_comm_group
220 section Z_bilin
221
222 variables {α : Type*} {β : Type*} {γ : Type*} {δ : Type*}
id └───┘ └───┘ └───┘
typ └───┘ └───┘ └───┘
223 variables [add_comm_group α] [add_comm_group β] [add_comm_group γ]
id └────────────┘ └────────────┘ └────────────┘
src └────────────┘ └────────────┘ └────────────┘
typ └────────────┘ └────────────┘ └────────────┘
224
225 /- TODO: when modules are changed to have more explicit base ring, then change replace `is_Z_bilin`
226 by using `is_bilinear_map ℤ` from `tensor_product`. -/
227 class is_Z_bilin (f : α × β → γ) : Prop :=
id ┴ ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴ ┴
228 (add_left : ∀ a a' b, f (a + a', b) = f (a, b) + f (a', b))
id ┴ └┘ ┴ ┴ ┴┴ ┴ └┘ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴└┘ ┴
src ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ └┘ ┴ ┴ ┴┴ ┴ └┘ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴└┘ ┴
229 (add_right : ∀ a b b', f (a, b + b') = f (a, b) + f (a, b'))
id ┴ ┴ └┘ ┴ ┴┴ ┴ ┴ └┘ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴┴ └┘
src ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ └┘ ┴ ┴┴ ┴ ┴ └┘ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴┴ └┘
230
231 variables (f : α × β → γ) [is_Z_bilin f]
id ┴ └────────┘
src ┴ └────────┘
typ ┴ └────────┘
232
233 instance is_Z_bilin.comp_hom {g : γ → δ} [add_comm_group δ] [is_add_group_hom g] :
id ┴ ┴ └────────────┘ ┴ └──────────────┘ ┴
src └────────────┘ └──────────────┘
typ ┴ ┴ └────────────┘ ┴ └──────────────┘ ┴
doc └──────────────┘
234 is_Z_bilin (g ∘ f) :=
id └────────┘ ┴ ┴ ┴
src └────────┘ ┴
typ └────────┘ ┴ ┴ ┴
235 by constructor; simp [(∘), is_Z_bilin.add_left f, is_Z_bilin.add_right f, is_add_hom.map_add g]
id ┴ └─────────────────┘ ┴ └──────────────────┘ ┴ └────────────────┘ ┴
src └─────────┘ └────┘┴└──┘└─────────────────┘┴ └┘└──────────────────┘┴ └┘└────────────────┘┴ └─
typ └─────────┘ └────┘┴└──┘└─────────────────┘┴┴└┘└──────────────────┘┴┴└┘└────────────────┘┴┴└─
doc └─────────┘ └────┘ └──┘ ┴ └┘ ┴ └┘ ┴ └─
txt └─────────┘ └────┘ └──┘ ┴ └┘ ┴ └┘ ┴ └─
par └─────────┘ └────┘ └──┘ ┴ └┘ ┴ └┘ ┴ └─
pid ┴┴ └──┘ ┴ └┘ ┴ └┘ ┴ ┴└
st └─────────────────────────────────────────────────────────────────────────────────────────────
236
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
237 instance is_Z_bilin.comp_swap : is_Z_bilin (f ∘ prod.swap) :=
id └────────┘ ┴ ┴ └───────┘
src └────────┘ ┴ └───────┘
typ └────────┘ ┴ ┴ └───────┘
doc └───────┘
238 ⟨λ a a' b, is_Z_bilin.add_right f b a a',
id ┴ └┘ ┴ └──────────────────┘ ┴ ┴ ┴ └┘
src └──────────────────┘
typ ┴ └┘ ┴ └──────────────────┘ ┴ ┴ ┴ └┘
239 λ a b b', is_Z_bilin.add_left f b b' a⟩
id ┴ ┴ └┘ └─────────────────┘ ┴ ┴ └┘ ┴
src └─────────────────┘
typ ┴ ┴ └┘ └─────────────────┘ ┴ ┴ └┘ ┴
240
241 lemma is_Z_bilin.zero_left : ∀ b, f (0, b) = 0 :=
id ┴ ┴ ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
242 begin
st └─────
243 intro b,
src └─────┘
typ └─────┘
doc └─────┘
txt └─────┘
par └─────┘
pid └┘
st ────────┘└─
244 apply add_self_iff_eq_zero.1,
id └──────────────────┘
src └────┘└──────────────────┘└┘
typ └────┘└──────────────────┘└┘
doc └────┘ └┘
txt └────┘ └┘
par └────┘ └┘
pid ┴ └┘
st ─────────────────────────────┘└─
245 rw ←is_Z_bilin.add_left f,
id └─────────────────┘ ┴
src └──┘└─────────────────┘┴
typ └──┘└─────────────────┘┴┴
doc └──┘ ┴
txt └──┘ ┴
par └──┘ ┴
pid └┘ ┴
st ──────────────────────────┘└─
246 simp
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
pid ┴
st ──────┘
247 end
st └─┘
248
249 lemma is_Z_bilin.zero_right : ∀ a, f (a, 0) = 0 :=
id ┴ ┴ ┴┴ ┴
src ┴ ┴
typ ┴ ┴ ┴┴ ┴
250 is_Z_bilin.zero_left (f ∘ prod.swap)
id └──────────────────┘ ┴ ┴ └───────┘
src └──────────────────┘ ┴ └───────┘
typ └──────────────────┘ ┴ ┴ └───────┘
doc └───────┘
251
252 lemma is_Z_bilin.zero : f (0, 0) = 0 :=
id ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴
253 is_Z_bilin.zero_left f 0
id └──────────────────┘ ┴
src └──────────────────┘
typ └──────────────────┘ ┴
254
255 lemma is_Z_bilin.neg_left : ∀ a b, f (-a, b) = -f (a, b) :=
id ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴┴ ┴┴ ┴
src ┴┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴┴ ┴┴ ┴
256 begin
st └─────
257 intros a b,
src └────────┘
typ └────────┘
doc └────────┘
txt └────────┘
par └────────┘
pid └──┘
st ───────────┘└─
258 apply eq_of_sub_eq_zero,
id └───────────────┘
src └────┘└───────────────┘
typ └────┘└───────────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ────────────────────────┘└─
259 rw [sub_eq_add_neg, neg_neg, ←is_Z_bilin.add_left f, neg_add_self, is_Z_bilin.zero_left f]
id └────────────┘ └─────┘ └─────────────────┘ ┴ └──────────┘ └──────────────────┘ ┴
src └──┘└────────────┘└┘└─────┘└─┘└─────────────────┘┴ └┘└──────────┘└┘└──────────────────┘┴ └┘
typ └──┘└────────────┘└┘└─────┘└─┘└─────────────────┘┴┴└┘└──────────┘└┘└──────────────────┘┴┴└┘
doc └──┘ └┘ └─┘ ┴ └┘ └┘ ┴ └┘
txt └──┘ └┘ └─┘ ┴ └┘ └┘ ┴ └┘
par └──┘ └┘ └─┘ ┴ └┘ └┘ ┴ └┘
pid └┘ └┘ └─┘ ┴ └┘ └┘ ┴ ┴┴
st ───────────────────┘└───────┘└──────────────────────┘└────────────┘└──────────────────────┘┴┴
260 end
st └─┘
261
262 lemma is_Z_bilin.neg_right : ∀ a b, f (a, -b) = -f (a, b) :=
id ┴ ┴ ┴ ┴┴ ┴┴ ┴ ┴┴ ┴┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴┴ ┴┴ ┴ ┴┴ ┴┴ ┴
263 assume a b, is_Z_bilin.neg_left (f ∘ prod.swap) b a
id ┴ ┴ └─────────────────┘ ┴ ┴ └───────┘ ┴ ┴
src └─────────────────┘ ┴ └───────┘
typ ┴ ┴ └─────────────────┘ ┴ ┴ └───────┘ ┴ ┴
doc └───────┘
264
265 lemma is_Z_bilin.sub_left : ∀ a a' b, f (a - a', b) = f (a, b) - f (a', b) :=
id ┴ └┘ ┴ ┴ ┴┴ ┴ └┘ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴└┘ ┴
src ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ └┘ ┴ ┴ ┴┴ ┴ └┘ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴└┘ ┴
266 begin
st └─────
267 intros,
src └────┘
typ └────┘
doc └────┘
txt └────┘
par └────┘
st ───────┘└─
268 dsimp [algebra.sub],
id └─────────┘
src └─────┘└─────────┘┴
typ └─────┘└─────────┘┴
doc └─────┘ ┴
txt └─────┘ ┴
par └─────┘ ┴
pid ┴┴ ┴
st ────────────────────┘└─
269 rw [is_Z_bilin.add_left f, is_Z_bilin.neg_left f]
id └─────────────────┘ ┴ └─────────────────┘ ┴
src └──┘└─────────────────┘┴ └┘└─────────────────┘┴ └┘
typ └──┘└─────────────────┘┴┴└┘└─────────────────┘┴┴└┘
doc └──┘ ┴ └┘ ┴ └┘
txt └──┘ ┴ └┘ ┴ └┘
par └──┘ ┴ └┘ ┴ └┘
pid └┘ ┴ └┘ ┴ ┴┴
st ──────────────────────────┘└─────────────────────┘┴┴
270 end
st └─┘
271
272 lemma is_Z_bilin.sub_right : ∀ a b b', f (a, b - b') = f (a, b) - f (a,b') :=
id ┴ ┴ └┘ ┴ ┴┴ ┴ ┴ └┘ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴┴ └┘
src ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ └┘ ┴ ┴┴ ┴ ┴ └┘ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴┴ └┘
273 assume a b b', is_Z_bilin.sub_left (f ∘ prod.swap) b b' a
id ┴ ┴ └┘ └─────────────────┘ ┴ ┴ └───────┘ ┴ └┘ ┴
src └─────────────────┘ ┴ └───────┘
typ ┴ ┴ └┘ └─────────────────┘ ┴ ┴ └───────┘ ┴ └┘ ┴
doc └───────┘
274 end Z_bilin
275 end add_comm_group
276
277 open add_comm_group filter set function
278
279 section
280 variables {α : Type*} {β : Type*} {γ : Type*} {δ : Type*}
281
282 -- α, β and G are abelian topological groups, G is a uniform space
283 variables [topological_space α] [add_comm_group α]
id └───────────────┘ └────────────┘
src └───────────────┘ └────────────┘
typ └───────────────┘ └────────────┘
doc └───────────────┘
284 variables [topological_space β] [add_comm_group β]
id └───────────────┘ └────────────┘
src └───────────────┘ └────────────┘
typ └───────────────┘ └────────────┘
doc └───────────────┘
285 variables {G : Type*} [uniform_space G] [add_comm_group G]
id └───────────┘ └────────────┘
src └───────────┘ └────────────┘
typ └───────────┘ └────────────┘
doc └───────────┘
286
287 variables {ψ : α × β → G} (hψ : continuous ψ) [ψbilin : is_Z_bilin ψ]
id ┴ └────────┘ └────────┘
src ┴ └────────┘ └────────┘
typ ┴ └────────┘ └────────┘
doc └────────┘
288
289 include hψ ψbilin
290
291 lemma is_Z_bilin.tendsto_zero_left (x₁ : α) : tendsto ψ (𝓝 (x₁, 0)) (𝓝 0) :=
id ┴ └─────┘ ┴ ┴ ┴└┘ ┴
src └─────┘ ┴ ┴ ┴
typ ┴ └─────┘ ┴ ┴ ┴└┘ ┴
doc └─────┘ ┴ ┴
292 begin
st └─────
293 have := hψ.tendsto (x₁, 0),
id └────────┘ ┴└┘
src └──────┘└────────┘┴┴ └──┘
typ └──────┘└────────┘┴┴└┘└──┘
doc └──────┘ ┴ └──┘
txt └──────┘ ┴ └──┘
par └──────┘ ┴ └──┘
pid └───┘└─┘ ┴ └──┘
st ───────────────────────────┘└─
294 rwa [is_Z_bilin.zero_right ψ] at this
id └───────────────────┘ ┴
src └───┘└───────────────────┘┴ └────────┘
typ └───┘└───────────────────┘┴┴└────────┘
doc └───┘ ┴ └────────┘
txt └───┘ ┴ └────────┘
par └───┘ ┴ └────────┘
pid └┘ ┴ ┴└──────┘┴
st ─────────────────────────────┘┴└───────┘
295 end
st └─┘
296
297 lemma is_Z_bilin.tendsto_zero_right (y₁ : β) : tendsto ψ (𝓝 (0, y₁)) (𝓝 0) :=
id ┴ └─────┘ ┴ ┴ ┴ └┘ ┴
src └─────┘ ┴ ┴ ┴
typ ┴ └─────┘ ┴ ┴ ┴ └┘ ┴
doc └─────┘ ┴ ┴
298 begin
st └─────
299 have := hψ.tendsto (0, y₁),
id └────────┘ ┴ └┘
src └──────┘└────────┘┴┴└─┘ ┴
typ └──────┘└────────┘┴┴└─┘└┘┴
doc └──────┘ ┴ └─┘ ┴
txt └──────┘ ┴ └─┘ ┴
par └──────┘ ┴ └─┘ ┴
pid └───┘└─┘ ┴ └─┘ ┴
st ───────────────────────────┘└─
300 rwa [is_Z_bilin.zero_left ψ] at this
id └──────────────────┘ ┴
src └───┘└──────────────────┘┴ └────────┘
typ └───┘└──────────────────┘┴┴└────────┘
doc └───┘ ┴ └────────┘
txt └───┘ ┴ └────────┘
par └───┘ ┴ └────────┘
pid └┘ ┴ ┴└──────┘┴
st ────────────────────────────┘┴└───────┘
301 end
st └─┘
302 end
303
304 section
305 variables {α : Type*} {β : Type*}
306 variables [topological_space α] [add_comm_group α] [topological_add_group α]
id └───────────────┘ ┴└────────────┘ └───────────────────┘
src └───────────────┘ └────────────┘ └───────────────────┘
typ └───────────────┘ ┴└────────────┘ └───────────────────┘
doc └───────────────┘ └───────────────────┘
307
308 -- β is a dense subgroup of α, inclusion is denoted by e
309 variables [topological_space β] [add_comm_group β]
id └───────────────┘ └────────────┘
src └───────────────┘ └────────────┘
typ └───────────────┘ └────────────┘
doc └───────────────┘
310 variables {e : β → α} [is_add_group_hom e] (de : dense_inducing e)
id └──────────────┘ └────────────┘
src └──────────────┘ └────────────┘
typ └──────────────┘ └────────────┘
doc └──────────────┘ └────────────┘
311 include de
312
313 lemma tendsto_sub_comap_self (x₀ : α) :
id ┴
typ ┴
314 tendsto (λt:β×β, t.2 - t.1) (comap (λp:β×β, (e p.1, e p.2)) $ 𝓝 (x₀, x₀)) (𝓝 0) :=
id └─────┘ ┴┴┴ ┴┴ ┴ ┴┴ └───┘ ┴┴┴ ┴┴ ┴┴ ┴ ┴┴ ┴ ┴└┘ └┘ ┴
src └─────┘ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ └─────┘ ┴┴┴ ┴┴ ┴ ┴┴ └───┘ ┴┴┴ ┴┴ ┴┴ ┴ ┴┴ ┴ ┴└┘ └┘ ┴
doc └─────┘ └───┘ ┴ ┴
315 begin
st └─────
316 have comm : (λx:α×α, x.2-x.1) ∘ (λt:β×β, (e t.1, e t.2)) = e ∘ (λt:β×β, t.2 - t.1),
id ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └──────────┘ └┘ ┴ └┘ └┘┴ └──┘┴┴ └┘ └┘┴ ┴ └──┘ ┴ └───┘┴┴ ┴ ┴ └┘ └┘ └─┘ ┴ └─┘
typ └──────────┘ └┘ ┴┴└┘ └┘┴ └──┘┴┴ └┘ ┴ └┘┴ ┴ └──┘ ┴ └───┘┴┴┴┴ ┴ └┘ ┴└┘ └─┘ ┴ └─┘
doc └──────────┘ └┘ └┘ └┘ └──┘ ┴ └┘ └┘ ┴ └──┘ ┴ └───┘ ┴ ┴ ┴ └┘ └┘ └─┘ ┴ └─┘
txt └──────────┘ └┘ └┘ └┘ └──┘ ┴ └┘ └┘ ┴ └──┘ ┴ └───┘ ┴ ┴ ┴ └┘ └┘ └─┘ ┴ └─┘
par └──────────┘ └┘ └┘ └┘ └──┘ ┴ └┘ └┘ ┴ └──┘ ┴ └───┘ ┴ ┴ ┴ └┘ └┘ └─┘ ┴ └─┘
pid └───────┘└─┘ └┘ └┘ └┘ └──┘ ┴ └┘ └┘ ┴ └──┘ ┴ └───┘ ┴ ┴ ┴ └┘ └┘ └─┘ ┴ └─┘
st ───────────────────────────────────────────────────────────────────────────────────┘└─
317 { ext t,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
pid └┘
st ───┘└───┘└─
318 change e t.2 - e t.1 = e (t.2 - t.1),
id ┴ ┴
src └─────┘ ┴ └─┘ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴ └─┘
typ └─────┘ ┴ └─┘ ┴ ┴ └─┘ ┴┴┴ └─┘ ┴┴└─┘
doc └─────┘ ┴ └─┘ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴ └─┘
txt └─────┘ ┴ └─┘ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴ └─┘
par └─────┘ ┴ └─┘ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴ └─┘
pid ┴ ┴ └─┘ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴ └─┘
st ───────────────────────────────────────┘└─
319 rwa ← is_add_group_hom.map_sub e t.2 t.1 },
id └──────────────────────┘ ┴ ┴
src └────┘└──────────────────────┘┴ ┴ └─┘ └─┘
typ └────┘└──────────────────────┘┴┴┴ └─┘┴└─┘
doc └────┘└──────────────────────┘┴ ┴ └─┘ └─┘
txt └────┘ ┴ ┴ └─┘ └─┘
par └────┘ ┴ ┴ └─┘ └─┘
pid └─┘ ┴ ┴ └─┘ └─┘
st ────────────────────────────────────────────┘└┘└
320 have lim : tendsto (λ x : α × α, x.2-x.1) (𝓝 (x₀, x₀)) (𝓝 (e 0)),
id └─────┘ ┴ ┴ ┴ └┘ ┴
src └─────────┘└─────┘┴ └───┘ ┴ ┴ └┘ └┘ └──┘ ┴┴┴ └┘ └─┘ ┴ └──┘
typ └─────────┘└─────┘┴ └───┘ ┴ ┴┴└┘ └┘ └──┘ ┴┴┴ └┘└┘└─┘ ┴ ┴└──┘
doc └─────────┘└─────┘┴ └───┘ ┴ ┴ └┘ └┘ └──┘ ┴┴ └┘ └─┘ ┴ └──┘
txt └─────────┘ ┴ └───┘ ┴ ┴ └┘ └┘ └──┘ ┴ └┘ └─┘ ┴ └──┘
par └─────────┘ ┴ └───┘ ┴ ┴ └┘ └┘ └──┘ ┴ └┘ └─┘ ┴ └──┘
pid └──────┘└─┘ ┴ └───┘ ┴ ┴ └┘ └┘ └──┘ ┴ └┘ └─┘ ┴ └──┘
st ─────────────────────────────────────────────────────────────────┘└─
321 { have := (continuous_sub.comp continuous_swap).tendsto (x₀, x₀),
id └─────────────────┘ └─────────────┘ ┴ └┘
src └──────┘ └─────────────────┘┴└─────────────┘└────────┘┴ └┘ ┴
typ └──────┘ └─────────────────┘┴└─────────────┘└────────┘┴ └┘└┘┴
doc └──────┘ ┴ └────────┘ └┘ ┴
txt └──────┘ ┴ └────────┘ └┘ ┴
par └──────┘ ┴ └────────┘ └┘ ┴
pid └───┘└─┘ ┴ └────────┘ └┘ ┴
st ─────┘└────────────────────────────────────────────────────────────┘└─
322 simpa [-sub_eq_add_neg, sub_self, eq.symm (is_add_group_hom.map_zero e)] using this },
id └──────┘ └─────┘ └───────────────────────┘ ┴ └──┘
src └──────────────────────┘└──────┘└┘└─────┘┴ └───────────────────────┘┴ └───────┘ ┴
typ └──────────────────────┘└──────┘└┘└─────┘┴ └───────────────────────┘┴┴└───────┘└──┘┴
doc └──────────────────────┘ └┘ ┴ ┴ └───────┘ ┴
txt └──────────────────────┘ └┘ ┴ ┴ └───────┘ ┴
par └──────────────────────┘ └┘ ┴ ┴ └───────┘ ┴
pid ┴└────────────────┘ └┘ ┴ ┴ └┘┴└────┘ ┴
st ─────────────────────────────────────────────────────────────────────────────────────────┘└┘└
323 have := de.tendsto_comap_nhds_nhds lim comm,
id └────────────────────────┘ └─┘ └──┘
src └──────┘└────────────────────────┘┴└─┘┴
typ └──────┘└────────────────────────┘┴└─┘┴└──┘
doc └──────┘└────────────────────────┘┴└─┘┴
txt └──────┘ ┴ ┴
par └──────┘ ┴ ┴
pid └───┘└─┘ ┴ ┴
st ────────────────────────────────────────────┘└─
324 simp [-sub_eq_add_neg, this]
id └──┘
src └─────────────────────┘ └┘
typ └─────────────────────┘└──┘└┘
doc └─────────────────────┘ └┘
txt └─────────────────────┘ └┘
par └─────────────────────┘ └┘
pid ┴└────────────────┘ ┴┴
st ──────────────────────────────┘
325 end
st └─┘
326 end
327
328 namespace dense_inducing
329 variables {α : Type*} {β : Type*} {γ : Type*} {δ : Type*}
330 variables {G : Type*}
331
332 -- β is a dense subgroup of α, inclusion is denoted by e
333 -- δ is a dense subgroup of γ, inclusion is denoted by f
334 variables [topological_space α] [add_comm_group α] [topological_add_group α]
id └───────────────┘ ┴└────────────┘ └───────────────────┘
src └───────────────┘ └────────────┘ └───────────────────┘
typ └───────────────┘ ┴└────────────┘ └───────────────────┘
doc └───────────────┘ └───────────────────┘
335 variables [topological_space β] [add_comm_group β] [topological_add_group β]
id └───────────────┘ └────────────┘ └───────────────────┘
src └───────────────┘ └────────────┘ └───────────────────┘
typ └───────────────┘ └────────────┘ └───────────────────┘
doc └───────────────┘ └───────────────────┘
336 variables [topological_space γ] [add_comm_group γ] [topological_add_group γ]
id └───────────────┘ └────────────┘ └───────────────────┘
src └───────────────┘ └────────────┘ └───────────────────┘
typ └───────────────┘ └────────────┘ └───────────────────┘
doc └───────────────┘ └───────────────────┘
337 variables [topological_space δ] [add_comm_group δ] [topological_add_group δ]
id └───────────────┘ └────────────┘ └───────────────────┘
src └───────────────┘ └────────────┘ └───────────────────┘
typ └───────────────┘ └────────────┘ └───────────────────┘
doc └───────────────┘ └───────────────────┘
338 variables [uniform_space G] [add_comm_group G] [uniform_add_group G] [separated G] [complete_space G]
id └───────────┘ └────────────┘ └───────────────┘ └───────┘ └────────────┘
src └───────────┘ └────────────┘ └───────────────┘ └───────┘ └────────────┘
typ └───────────┘ └────────────┘ └───────────────┘ └───────┘ └────────────┘
doc └───────────┘ └───────────────┘ └────────────┘
339 variables {e : β → α} [is_add_group_hom e] (de : dense_inducing e)
id └──────────────┘ └────────────┘
src └──────────────┘ └────────────┘
typ └──────────────┘ └────────────┘
doc └──────────────┘ └────────────┘
340 variables {f : δ → γ} [is_add_group_hom f] (df : dense_inducing f)
id └──────────────┘ └────────────┘
src └──────────────┘ └────────────┘
typ └──────────────┘ └────────────┘
doc └──────────────┘ └────────────┘
341 variables {φ : β × δ → G} (hφ : continuous φ) [bilin : is_Z_bilin φ]
id ┴ └────────┘ └────────┘
src ┴ └────────┘ └────────┘
typ ┴ └────────┘ └────────┘
doc └────────┘
342
343 include de df hφ bilin
344
345 variables {W' : set G} (W'_nhd : W' ∈ 𝓝 (0 : G))
id └─┘ ┴ ┴
src └─┘ ┴ ┴
typ └─┘ ┴ ┴
doc ┴
346 include W'_nhd
347
348 private lemma extend_Z_bilin_aux (x₀ : α) (y₁ : δ) :
id ┴ ┴
typ ┴ ┴
349 ∃ U₂ ∈ comap e (𝓝 x₀), ∀ x x' ∈ U₂, φ (x' - x, y₁) ∈ W' :=
id ┴ └┘ └───┘ ┴ ┴ └┘ ┴ ┴ └┘ └┘ ┴ ┴└┘ ┴ ┴ └┘ ┴ └┘
src ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ └┘ └───┘ ┴ ┴ └┘ ┴ ┴ └┘ └┘ ┴ ┴└┘ ┴ ┴ └┘ ┴ └┘
doc └───┘ ┴
350 begin
st └─────
351 let Nx := 𝓝 x₀,
id ┴ └┘
src └────────┘┴┴
typ └────────┘┴┴└┘
doc └────────┘┴┴
txt └────────┘ ┴
par └────────┘ ┴
pid └────┘┴└─┘ ┴
st ───────────────┘└─
352 let ee := λ u : β × β, (e u.1, e u.2),
id ┴ ┴ ┴ ┴
src └────────┘ └───┘ ┴┴┴ └┘┴ ┴ └──┘ ┴ └─┘
typ └────────┘ └───┘ ┴┴┴┴└┘┴ ┴ └──┘┴┴ └─┘
doc └────────┘ └───┘ ┴ ┴ └┘ ┴ └──┘ ┴ └─┘
txt └────────┘ └───┘ ┴ ┴ └┘ ┴ └──┘ ┴ └─┘
par └────────┘ └───┘ ┴ ┴ └┘ ┴ └──┘ ┴ └─┘
pid └────┘┴└─┘ └───┘ ┴ ┴ └┘ ┴ └──┘ ┴ └─┘
st ──────────────────────────────────────┘└─
353
st ─
354 have lim1 : tendsto (λ a : β × β, (a.2 - a.1, y₁)) (filter.prod (comap e Nx) (comap e Nx)) (𝓝 (0, y₁)),
id └─────┘ ┴ ┴ └─────────┘ └───┘ ┴ └┘ ┴ └┘
src └──────────┘└─────┘┴ └───┘ ┴ ┴ └┘ └─┘┴┴ └──┘ └─┘ └─────────┘┴ ┴ ┴ └┘ └───┘┴ ┴ └─┘ ┴┴└─┘ └┘
typ └──────────┘└─────┘┴ └───┘ ┴ ┴┴└┘ └─┘┴┴ └──┘ └─┘ └─────────┘┴ ┴ ┴ └┘ └───┘┴┴┴└┘└─┘ ┴┴└─┘└┘└┘
doc └──────────┘└─────┘┴ └───┘ ┴ ┴ └┘ └─┘ ┴ └──┘ └─┘ └─────────┘┴ ┴ ┴ └┘ └───┘┴ ┴ └─┘ ┴ └─┘ └┘
txt └──────────┘ ┴ └───┘ ┴ ┴ └┘ └─┘ ┴ └──┘ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ └─┘ ┴ └─┘ └┘
par └──────────┘ ┴ └───┘ ┴ ┴ └┘ └─┘ ┴ └──┘ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ └─┘ ┴ └─┘ └┘
pid └───────┘└─┘ ┴ └───┘ ┴ ┴ └┘ └─┘ ┴ └──┘ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ └─┘ ┴ └─┘ └┘
st ───────────────────────────────────────────────────────────────────────────────────────────────────────┘└─
355 { have := tendsto.prod_mk (tendsto_sub_comap_self de x₀) (tendsto_const_nhds : tendsto (λ (p : β × β), y₁) (comap ee $ 𝓝 (x₀, x₀)) (𝓝 y₁)),
id └─────────────┘ └────────────────────┘ └┘ └────────────────┘ └─────┘ ┴ └───┘ └┘ ┴ └┘ └┘
src └──────┘└─────────────┘┴ └────────────────────┘┴ ┴ └┘ └────────────────┘└─┘└─────┘┴ └────┘ ┴ ┴ └─┘ └┘ └───┘┴ ┴ ┴ ┴┴ └┘ └─┘ ┴ └┘
typ └──────┘└─────────────┘┴ └────────────────────┘┴└┘┴ └┘ └────────────────┘└─┘└─────┘┴ └────┘ ┴ ┴┴└─┘ └┘ └───┘┴└┘┴ ┴ ┴┴ └┘└┘└─┘ ┴└┘└┘
doc └──────┘ ┴ ┴ ┴ └┘ └─┘└─────┘┴ └────┘ ┴ ┴ └─┘ └┘ └───┘┴ ┴ ┴ ┴ └┘ └─┘ ┴ └┘
txt └──────┘ ┴ ┴ ┴ └┘ └─┘ ┴ └────┘ ┴ ┴ └─┘ └┘ ┴ ┴ ┴ ┴ └┘ └─┘ ┴ └┘
par └──────┘ ┴ ┴ ┴ └┘ └─┘ ┴ └────┘ ┴ ┴ └─┘ └┘ ┴ ┴ ┴ ┴ └┘ └─┘ ┴ └┘
pid └───┘└─┘ ┴ ┴ ┴ └┘ └─┘ ┴ └────┘ ┴ ┴ └─┘ └┘ ┴ ┴ ┴ ┴ └┘ └─┘ ┴ └┘
st ───┘└──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘└─
356 rw [nhds_prod_eq, prod_comap_comap_eq, ←nhds_prod_eq],
id └──────────┘ └─────────────────┘ └──────────┘
src └──┘└──────────┘└┘└─────────────────┘└─┘└──────────┘┴
typ └──┘└──────────┘└┘└─────────────────┘└─┘└──────────┘┴
doc └──┘ └┘ └─┘ ┴
txt └──┘ └┘ └─┘ ┴
par └──┘ └┘ └─┘ ┴
pid └┘ └┘ └─┘ ┴
st ───────────────────┘└───────────────────┘└─────────────┘└──
357 exact (this : _) },
id └──┘
src └────┘ └────┘
typ └────┘ └──┘└────┘
doc └────┘ └────┘
txt └────┘ └────┘
par └────┘ └────┘
pid ┴ └───┘┴
st ────────────────────┘└┘└
358
st ─
359 have lim := tendsto.comp (is_Z_bilin.tendsto_zero_right hφ y₁) lim1,
id └──────────┘ └───────────────────────────┘ └┘ └┘ └──┘
src └──────────┘└──────────┘┴ └───────────────────────────┘┴ ┴ └┘
typ └──────────┘└──────────┘┴ └───────────────────────────┘┴└┘┴└┘└┘└──┘
doc └──────────┘ ┴ ┴ ┴ └┘
txt └──────────┘ ┴ ┴ ┴ └┘
par └──────────┘ ┴ ┴ ┴ └┘
pid └──────┘┴└─┘ ┴ ┴ ┴ └┘
st ────────────────────────────────────────────────────────────────────┘└─
360 rw tendsto_prod_self_iff at lim,
id └───────────────────┘
src └─┘└───────────────────┘└─────┘
typ └─┘└───────────────────┘└─────┘
doc └─┘ └─────┘
txt └─┘ └─────┘
par └─┘ └─────┘
pid ┴ └─────┘
st ────────────────────────────────┘└─
361 exact lim W' W'_nhd,
id └─┘ └┘ └────┘
src └────┘└─┘┴ ┴
typ └────┘└─┘┴└┘┴└────┘
doc └────┘└─┘┴ ┴
txt └────┘ ┴ ┴
par └────┘ ┴ ┴
pid ┴ ┴ ┴
st ────────────────────┘└─
362 end
st ──┘
363
364 private lemma extend_Z_bilin_key (x₀ : α) (y₀ : γ) :
id ┴ ┴
typ ┴ ┴
365 ∃ U ∈ comap e (𝓝 x₀), ∃ V ∈ comap f (𝓝 y₀),
id ┴ ┴ └───┘ ┴ ┴ └┘ ┴ ┴ ┴ └───┘ ┴ ┴ └┘ ┴
src ┴ └───┘ ┴ ┴ ┴ └───┘ ┴ ┴
typ ┴ ┴ └───┘ ┴ ┴ └┘ ┴ ┴ ┴ └───┘ ┴ ┴ └┘ ┴
doc └───┘ ┴ └───┘ ┴
366 ∀ x x' ∈ U, ∀ y y' ∈ V, φ (x', y') - φ (x, y) ∈ W' :=
id ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴└┘ └┘ ┴ ┴ ┴┴ ┴ ┴ └┘
src ┴ ┴ ┴ ┴
typ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴└┘ └┘ ┴ ┴ ┴┴ ┴ ┴ └┘
367 begin
st └─────
368 let Nx := 𝓝 x₀,
id ┴ └┘
src └────────┘┴┴
typ └────────┘┴┴└┘
doc └────────┘┴┴
txt └────────┘ ┴
par └────────┘ ┴
pid └────┘┴└─┘ ┴
st ───────────────┘└─
369 let Ny := 𝓝 y₀,
id └┘
src └────────┘ ┴
typ └────────┘ ┴└┘
doc └────────┘ ┴
txt └────────┘ ┴
par └────────┘ ┴
pid └────┘┴└─┘ ┴
st ───────────────┘└─
370 let dp := dense_inducing.prod de df,
id └─────────────────┘ └┘ └┘
src └────────┘└─────────────────┘┴ ┴
typ └────────┘└─────────────────┘┴└┘┴└┘
doc └────────┘└─────────────────┘┴ ┴
txt └────────┘ ┴ ┴
par └────────┘ ┴ ┴
pid └────┘┴└─┘ ┴ ┴
st ────────────────────────────────────┘└─
371 let ee := λ u : β × β, (e u.1, e u.2),
id ┴ ┴ ┴ ┴
src └────────┘ └───┘ ┴┴┴ └┘┴ ┴ └──┘ ┴ └─┘
typ └────────┘ └───┘ ┴┴┴┴└┘┴ ┴ └──┘┴┴ └─┘
doc └────────┘ └───┘ ┴ ┴ └┘ ┴ └──┘ ┴ └─┘
txt └────────┘ └───┘ ┴ ┴ └┘ ┴ └──┘ ┴ └─┘
par └────────┘ └───┘ ┴ ┴ └┘ ┴ └──┘ ┴ └─┘
pid └────┘┴└─┘ └───┘ ┴ ┴ └┘ ┴ └──┘ ┴ └─┘
st ──────────────────────────────────────┘└─
372 let ff := λ u : δ × δ, (f u.1, f u.2),
id ┴ ┴ ┴ ┴
src └────────┘ └───┘ ┴ ┴ └┘┴ ┴ └──┘ ┴ └─┘
typ └────────┘ └───┘ ┴┴┴┴└┘┴ ┴ └──┘┴┴ └─┘
doc └────────┘ └───┘ ┴ ┴ └┘ ┴ └──┘ ┴ └─┘
txt └────────┘ └───┘ ┴ ┴ └┘ ┴ └──┘ ┴ └─┘
par └────────┘ └───┘ ┴ ┴ └┘ ┴ └──┘ ┴ └─┘
pid └────┘┴└─┘ └───┘ ┴ ┴ └┘ ┴ └──┘ ┴ └─┘
st ──────────────────────────────────────┘└─
373
st ─
374 have lim_φ : filter.tendsto φ (𝓝 (0, 0)) (𝓝 0),
id └────────────┘ ┴ ┴
src └───────────┘└────────────┘┴ ┴ ┴┴└─────┘ └─┘
typ └───────────┘└────────────┘┴┴┴ ┴┴└─────┘ └─┘
doc └───────────┘└────────────┘┴ ┴ ┴ └─────┘ └─┘
txt └───────────┘ ┴ ┴ ┴ └─────┘ └─┘
par └───────────┘ ┴ ┴ ┴ └─────┘ └─┘
pid └────────┘└─┘ ┴ ┴ ┴ └─────┘ └─┘
st ───────────────────────────────────────────────┘└─
375 { have := hφ.tendsto (0, 0),
id └────────┘ ┴
src └──────┘└────────┘┴┴└───┘
typ └──────┘└────────┘┴┴└───┘
doc └──────┘ ┴ └───┘
txt └──────┘ ┴ └───┘
par └──────┘ ┴ └───┘
pid └───┘└─┘ ┴ └───┘
st ───┘└───────────────────────┘└─
376 rwa [is_Z_bilin.zero φ] at this },
id └─────────────┘ ┴
src └───┘└─────────────┘┴ └────────┘
typ └───┘└─────────────┘┴┴└────────┘
doc └───┘ ┴ └────────┘
txt └───┘ ┴ └────────┘
par └───┘ ┴ └────────┘
pid └┘ ┴ ┴└──────┘┴
st ─────────────────────────┘┴└───────┘└┘└
377
st ─
378 have lim_φ_sub_sub : tendsto (λ (p : (β × β) × (δ × δ)), φ (p.1.2 - p.1.1, p.2.2 - p.2.1))
id └─────┘ ┴ ┴ ┴ ┴ ┴
src └───────────────────┘└─────┘┴ └────┘ ┴ ┴ └┘ ┴ ┴ ┴ └──┘ ┴ └───┘┴┴ └────┘ └───┘ ┴ └──────
typ └───────────────────┘└─────┘┴ └────┘ ┴ ┴┴└┘┴┴ ┴ ┴┴└──┘┴┴ └───┘┴┴ └────┘ └───┘ ┴ └──────
doc └───────────────────┘└─────┘┴ └────┘ ┴ ┴ └┘ ┴ ┴ ┴ └──┘ ┴ └───┘ ┴ └────┘ └───┘ ┴ └──────
txt └───────────────────┘ ┴ └────┘ ┴ ┴ └┘ ┴ ┴ ┴ └──┘ ┴ └───┘ ┴ └────┘ └───┘ ┴ └──────
par └───────────────────┘ ┴ └────┘ ┴ ┴ └┘ ┴ ┴ ┴ └──┘ ┴ └───┘ ┴ └────┘ └───┘ ┴ └──────
pid └────────────────┘└─┘ ┴ └────┘ ┴ ┴ └┘ ┴ ┴ ┴ └──┘ ┴ └───┘ ┴ └────┘ └───┘ ┴ └──────
st ─────────────────────────────────────────────────────────────────────────────────────────────
379 (filter.prod (comap ee $ 𝓝 (x₀, x₀)) (comap ff $ 𝓝 (y₀, y₀))) (𝓝 0),
id └─────────┘ └┘ └┘ └───┘ └┘ ┴ └┘
src ───┘ └─────────┘┴ ┴ ┴ ┴ ┴ └┘ └─┘ └───┘┴ ┴ ┴ ┴┴ └┘ └──┘ └─┘
typ ───┘ └─────────┘┴ ┴└┘┴ ┴ ┴ └┘└┘└─┘ └───┘┴└┘┴ ┴ ┴┴ └┘└┘└──┘ └─┘
doc ───┘ └─────────┘┴ ┴ ┴ ┴ ┴ └┘ └─┘ └───┘┴ ┴ ┴ ┴ └┘ └──┘ └─┘
txt ───┘ ┴ ┴ ┴ ┴ ┴ └┘ └─┘ ┴ ┴ ┴ ┴ └┘ └──┘ └─┘
par ───┘ ┴ ┴ ┴ ┴ ┴ └┘ └─┘ ┴ ┴ ┴ ┴ └┘ └──┘ └─┘
pid ───┘ ┴ ┴ ┴ ┴ ┴ └┘ └─┘ ┴ ┴ ┴ ┴ └┘ └──┘ └─┘
st ──────────────────────────────────────────────────────────────────────┘└─
380 { have lim_sub_sub : tendsto (λ (p : (β × β) × δ × δ), (p.1.2 - p.1.1, p.2.2 - p.2.1))
id └─────┘ ┴ ┴
src └──────────────────┘└─────┘┴ └────┘ ┴ ┴ └┘ ┴ ┴ ┴ └─┘ └───┘ ┴ └────┘ └───┘ ┴ └──────
typ └──────────────────┘└─────┘┴ └────┘ ┴ ┴┴└┘ ┴ ┴ ┴┴└─┘ └───┘ ┴ └────┘ └───┘ ┴ └──────
doc └──────────────────┘└─────┘┴ └────┘ ┴ ┴ └┘ ┴ ┴ ┴ └─┘ └───┘ ┴ └────┘ └───┘ ┴ └──────
txt └──────────────────┘ ┴ └────┘ ┴ ┴ └┘ ┴ ┴ ┴ └─┘ └───┘ ┴ └────┘ └───┘ ┴ └──────
par └──────────────────┘ ┴ └────┘ ┴ ┴ └┘ ┴ ┴ ┴ └─┘ └───┘ ┴ └────┘ └───┘ ┴ └──────
pid └──────────────┘└──┘ ┴ └────┘ ┴ ┴ └┘ ┴ ┴ ┴ └─┘ └───┘ ┴ └────┘ └───┘ ┴ └──────
st ───┘└─────────────────────────────────────────────────────────────────────────────────────
381 (filter.prod (comap ee (𝓝 (x₀, x₀))) (comap ff (𝓝 (y₀, y₀)))) (filter.prod (𝓝 0) (𝓝 0)),
id └┘ └┘ └───┘ └┘ ┴ └┘ └─────────┘
src ─────┘ ┴ ┴ ┴ ┴ └┘ └──┘ └───┘┴ ┴ ┴┴ └┘ └───┘ └─────────┘┴ └──┘ └──┘
typ ─────┘ ┴ ┴└┘┴ ┴ └┘└┘└──┘ └───┘┴└┘┴ ┴┴ └┘└┘└───┘ └─────────┘┴ └──┘ └──┘
doc ─────┘ ┴ ┴ ┴ ┴ └┘ └──┘ └───┘┴ ┴ ┴ └┘ └───┘ └─────────┘┴ └──┘ └──┘
txt ─────┘ ┴ ┴ ┴ ┴ └┘ └──┘ ┴ ┴ ┴ └┘ └───┘ ┴ └──┘ └──┘
par ─────┘ ┴ ┴ ┴ ┴ └┘ └──┘ ┴ ┴ ┴ └┘ └───┘ ┴ └──┘ └──┘
pid ─────┘ ┴ ┴ ┴ ┴ └┘ └──┘ ┴ ┴ ┴ └┘ └───┘ ┴ └──┘ └──┘
st ────────────────────────────────────────────────────────────────────────────────────────────┘└─
382 { have := filter.prod_mono (tendsto_sub_comap_self de x₀) (tendsto_sub_comap_self df y₀),
id └──────────────┘ └┘ └┘ └────────────────────┘ └┘ └┘
src └──────┘└──────────────┘┴ ┴ ┴ └┘ └────────────────────┘┴ ┴ ┴
typ └──────┘└──────────────┘┴ ┴└┘┴└┘└┘ └────────────────────┘┴└┘┴└┘┴
doc └──────┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴
txt └──────┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴
par └──────┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴
pid └───┘└─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴
st ─────┘└────────────────────────────────────────────────────────────────────────────────────┘└─
383 rwa prod_map_map_eq at this },
id └─────────────┘
src └──┘└─────────────┘└───────┘
typ └──┘└─────────────┘└───────┘
doc └──┘ └───────┘
txt └──┘ └───────┘
par └──┘ └───────┘
pid ┴ └──────┘┴
st ─────────────────────────────────┘└┘└
384 rw ← nhds_prod_eq at lim_sub_sub,
id └──────────┘
src └───┘└──────────┘└─────────────┘
typ └───┘└──────────┘└─────────────┘
doc └───┘ └─────────────┘
txt └───┘ └─────────────┘
par └───┘ └─────────────┘
pid └─┘ └─────────────┘
st ───────────────────────────────────┘└─
385 exact tendsto.comp lim_φ lim_sub_sub },
id └──────────┘ └───┘ └─────────┘
src └────┘└──────────┘┴ ┴ ┴
typ └────┘└──────────┘┴└───┘┴└─────────┘┴
doc └────┘ ┴ ┴ ┴
txt └────┘ ┴ ┴ ┴
par └────┘ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴
st ────────────────────────────────────────┘└┘└
386
st ─
387 rcases exists_nhds_quarter W'_nhd with ⟨W, W_nhd, W4⟩,
id └─────────────────┘ └────┘
src └─────┘└─────────────────┘┴ └──────────────────┘
typ └─────┘└─────────────────┘┴└────┘└──────────────────┘
doc └─────┘ ┴ └──────────────────┘
txt └─────┘ ┴ └──────────────────┘
par └─────┘ ┴ └──────────────────┘
pid ┴ ┴ └──────────────────┘
st ──────────────────────────────────────────────────────┘└─
388
st ─
389 have : ∃ U₁ ∈ comap e (𝓝 x₀), ∃ V₁ ∈ comap f (𝓝 y₀),
id ┴ ┴ └┘ ┴ └───┘ ┴ └┘
src └─────┘┴└────┘ ┴ ┴ ┴ ┴┴┴ └────┘└───┘┴ ┴ ┴ ┴ └
typ └─────┘┴└────┘ ┴┴┴ ┴└┘┴┴┴ └────┘└───┘┴┴┴ ┴└┘┴ └
doc └─────┘ └────┘ ┴ ┴ ┴ ┴ ┴ └────┘└───┘┴ ┴ ┴ ┴ └
txt └─────┘ └────┘ ┴ ┴ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ └
par └─────┘ └────┘ ┴ ┴ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ └
pid └───┘└┘ └────┘ ┴ ┴ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ └
st ───────────────────────────────────────────────────────
390 ∀ x x' ∈ U₁, ∀ y y' ∈ V₁, φ (x'-x, y'-y) ∈ W,
id ┴ ┴ ┴
src ───┘ └──────┘ ┴ └──────┘ └┘ ┴┴ └┘ └┘ ┴
typ ───┘ └──────┘ ┴ └──────┘ └┘┴┴┴ └┘ └┘ ┴┴
doc ───┘ └──────┘ ┴ └──────┘ └┘ ┴ └┘ └┘ ┴
txt ───┘ └──────┘ ┴ └──────┘ └┘ ┴ └┘ └┘ ┴
par ───┘ └──────┘ ┴ └──────┘ └┘ ┴ └┘ └┘ ┴
pid ───┘ └──────┘ ┴ └──────┘ └┘ ┴ └┘ └┘ ┴
st ────────────────────────────────────────────────┘└─
391 { have := tendsto_prod_iff.1 lim_φ_sub_sub W W_nhd,
id └──────────────┘ └───────────┘ ┴ └───┘
src └──────┘└──────────────┘└─┘ ┴ ┴
typ └──────┘└──────────────┘└─┘└───────────┘┴┴┴└───┘
doc └──────┘ └─┘ ┴ ┴
txt └──────┘ └─┘ ┴ ┴
par └──────┘ └─┘ ┴ ┴
pid └───┘└─┘ └─┘ ┴ ┴
st ───┘└──────────────────────────────────────────────┘└─
392 repeat { rw [nhds_prod_eq, ←prod_comap_comap_eq] at this },
id └──────────┘ └─────────────────┘
src └───────┘└──┘└──────────┘└─┘└─────────────────┘└────────┘┴
typ └───────┘└──┘└──────────┘└─┘└─────────────────┘└────────┘┴
doc └───────┘└──┘ └─┘ └────────┘┴
txt └───────┘└──┘ └─┘ └────────┘┴
par └───────┘└──┘ └─┘ └────────┘┴
pid └─────┘ └─┘ └─────────┘
st ────────────────────────────┘└────────────────────┘┴└───────┘└┘└
393 rcases this with ⟨U, U_in, V, V_in, H⟩,
id └──┘
src └─────┘ └─────────────────────────┘
typ └─────┘└──┘└─────────────────────────┘
doc └─────┘ └─────────────────────────┘
txt └─────┘ └─────────────────────────┘
par └─────┘ └─────────────────────────┘
pid ┴ └─────────────────────────┘
st ─────────────────────────────────────────┘└─
394 rw [mem_prod_same_iff] at U_in V_in,
id └───────────────┘
src └──┘└───────────────┘└────────────┘
typ └──┘└───────────────┘└────────────┘
doc └──┘ └────────────┘
txt └──┘ └────────────┘
par └──┘ └────────────┘
pid └┘ ┴└───────────┘
st ────────────────────────┘┴└───────────┘└─
395 rcases U_in with ⟨U₁, U₁_in, HU₁⟩,
id └──┘
src └─────┘ └────────────────────┘
typ └─────┘└──┘└────────────────────┘
doc └─────┘ └────────────────────┘
txt └─────┘ └────────────────────┘
par └─────┘ └────────────────────┘
pid ┴ └────────────────────┘
st ────────────────────────────────────┘└─
396 rcases V_in with ⟨V₁, V₁_in, HV₁⟩,
id └──┘
src └─────┘ └────────────────────┘
typ └─────┘└──┘└────────────────────┘
doc └─────┘ └────────────────────┘
txt └─────┘ └────────────────────┘
par └─────┘ └────────────────────┘
pid ┴ └────────────────────┘
st ────────────────────────────────────┘└─
397 existsi [U₁, U₁_in, V₁, V₁_in],
id └┘ └───┘ └┘ └───┘
src └───────┘ └┘ └┘ └┘ ┴
typ └───────┘└┘└┘└───┘└┘└┘└┘└───┘┴
doc └───────┘ └┘ └┘ └┘ ┴
txt └───────┘ └┘ └┘ └┘ ┴
par └───────┘ └┘ └┘ └┘ ┴
pid └┘ └┘ └┘ └┘ ┴
st ─────────────────────────────────┘└─
398 intros x x' x_in x'_in y y' y_in y'_in,
src └────────────────────────────────────┘
typ └────────────────────────────────────┘
doc └────────────────────────────────────┘
txt └────────────────────────────────────┘
par └────────────────────────────────────┘
pid └──────────────────────────────┘
st ─────────────────────────────────────────┘└─
399 exact H _ _ (HU₁ (mk_mem_prod x_in x'_in)) (HV₁ (mk_mem_prod y_in y'_in)) },
id ┴ └─┘ └──┘ └───┘ └─┘ └─────────┘ └──┘ └───┘
src └────┘ └───┘ ┴ ┴ ┴ └─┘ ┴ └─────────┘┴ ┴ └─┘
typ └────┘┴└───┘ └─┘┴ ┴└──┘┴└───┘└─┘ └─┘┴ └─────────┘┴└──┘┴└───┘└─┘
doc └────┘ └───┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └─┘
txt └────┘ └───┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └─┘
par └────┘ └───┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └─┘
pid ┴ └───┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └┘┴
st ─────────────────────────────────────────────────────────────────────────────┘└┘└
400 rcases this with ⟨U₁, U₁_nhd, V₁, V₁_nhd, H⟩,
id └──┘
src └─────┘ └───────────────────────────────┘
typ └─────┘└──┘└───────────────────────────────┘
doc └─────┘ └───────────────────────────────┘
txt └─────┘ └───────────────────────────────┘
par └─────┘ └───────────────────────────────┘
pid ┴ └───────────────────────────────┘
st ─────────────────────────────────────────────┘└─
401
st ─
402 obtain ⟨x₁, x₁_in⟩ : U₁.nonempty :=
id └─────────┘
src └───────────────────┘└─────────┘└───
typ └───────────────────┘└─────────┘└───
doc └───────────────────┘└─────────┘└───
txt └───────────────────┘ └───
par └───────────────────┘ └───
pid └─────────────┘ └───
st ──────────────────────────────────────
403 (forall_sets_nonempty_iff_ne_bot.2 de.comap_nhds_ne_bot U₁ U₁_nhd),
id └─────────────────────────────┘ └──────────────────┘ └┘ └────┘
src ───┘ └─────────────────────────────┘└─┘└──────────────────┘┴ ┴ ┴
typ ───┘ └─────────────────────────────┘└─┘└──────────────────┘┴└┘┴└────┘┴
doc ───┘ └─┘ ┴ ┴ ┴
txt ───┘ └─┘ ┴ ┴ ┴
par ───┘ └─┘ ┴ ┴ ┴
pid ───┘ └─┘ ┴ ┴ ┴
st ─────────────────────────────────────────────────────────────────────┘└─
404 obtain ⟨y₁, y₁_in⟩ : V₁.nonempty :=
id └─────────┘
src └───────────────────┘└─────────┘└───
typ └───────────────────┘└─────────┘└───
doc └───────────────────┘└─────────┘└───
txt └───────────────────┘ └───
par └───────────────────┘ └───
pid └─────────────┘ └───
st ──────────────────────────────────────
405 (forall_sets_nonempty_iff_ne_bot.2 df.comap_nhds_ne_bot V₁ V₁_nhd),
id └─────────────────────────────┘ └──────────────────┘ └┘ └────┘
src ───┘ └─────────────────────────────┘└─┘└──────────────────┘┴ ┴ ┴
typ ───┘ └─────────────────────────────┘└─┘└──────────────────┘┴└┘┴└────┘┴
doc ───┘ └─┘ ┴ ┴ ┴
txt ───┘ └─┘ ┴ ┴ ┴
par ───┘ └─┘ ┴ ┴ ┴
pid ───┘ └─┘ ┴ ┴ ┴
st ─────────────────────────────────────────────────────────────────────┘└─
406
st ─
407 rcases (extend_Z_bilin_aux de df hφ W_nhd x₀ y₁) with ⟨U₂, U₂_nhd, HU⟩,
id └────────────────┘ └┘ └┘ └┘ └───┘ └┘ └┘
src └─────┘ └────────────────┘┴ ┴ ┴ ┴ ┴ ┴ └─────────────────────┘
typ └─────┘ └────────────────┘┴└┘┴└┘┴└┘┴└───┘┴└┘┴└┘└─────────────────────┘
doc └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─────────────────────┘
txt └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─────────────────────┘
par └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─────────────────────┘
pid ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────────────────────┘
st ───────────────────────────────────────────────────────────────────────┘└─
408 rcases (extend_Z_bilin_aux df de (hφ.comp continuous_swap) W_nhd y₀ x₁) with ⟨V₂, V₂_nhd, HV⟩,
id └────────────────┘ └┘ └┘ └─────┘ └─────────────┘ └───┘ └┘ └┘
src └─────┘ └────────────────┘┴ ┴ ┴ └─────┘┴└─────────────┘└┘ ┴ ┴ └─────────────────────┘
typ └─────┘ └────────────────┘┴└┘┴└┘┴ └─────┘┴└─────────────┘└┘└───┘┴└┘┴└┘└─────────────────────┘
doc └─────┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └─────────────────────┘
txt └─────┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └─────────────────────┘
par └─────┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └─────────────────────┘
pid ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └─────────────────────┘
st ──────────────────────────────────────────────────────────────────────────────────────────────┘└─
409
st ─
410 existsi [U₁ ∩ U₂, inter_mem_sets U₁_nhd U₂_nhd,
id └┘ ┴ └┘ └────────────┘ └────┘ └────┘
src └───────┘ ┴┴┴ └┘└────────────┘┴ ┴ └─
typ └───────┘└┘┴┴┴└┘└┘└────────────┘┴└────┘┴└────┘└─
doc └───────┘ ┴ ┴ └┘ ┴ ┴ └─
txt └───────┘ ┴ ┴ └┘ ┴ ┴ └─
par └───────┘ ┴ ┴ └┘ ┴ ┴ └─
pid └┘ ┴ ┴ └┘ ┴ ┴ └─
st ──────────────────────────────────────────────────
411 V₁ ∩ V₂, inter_mem_sets V₁_nhd V₂_nhd],
id └┘ └┘ └────────────┘ └────┘ └────┘
src ───────────┘ ┴ ┴ └┘└────────────┘┴ ┴ ┴
typ ───────────┘└┘┴ ┴└┘└┘└────────────┘┴└────┘┴└────┘┴
doc ───────────┘ ┴ ┴ └┘ ┴ ┴ ┴
txt ───────────┘ ┴ ┴ └┘ ┴ ┴ ┴
par ───────────┘ ┴ ┴ └┘ ┴ ┴ ┴
pid ───────────┘ ┴ ┴ └┘ ┴ ┴ ┴
st ─────────────────────────────────────────────────┘└─
412
st ─
413 rintros x x' ⟨xU₁, xU₂⟩ ⟨x'U₁, x'U₂⟩ y y' ⟨yV₁, yV₂⟩ ⟨y'V₁, y'V₂⟩,
src └───────────────────────────────────────────────────────────────┘
typ └───────────────────────────────────────────────────────────────┘
doc └───────────────────────────────────────────────────────────────┘
txt └───────────────────────────────────────────────────────────────┘
par └───────────────────────────────────────────────────────────────┘
pid └────────────────────────────────────────────────────────┘
st ──────────────────────────────────────────────────────────────────┘└─
414 have key_formula : φ(x', y') - φ(x, y) = φ(x' - x, y₁) + φ(x' - x, y' - y₁) + φ(x₁, y' - y) + φ(x - x₁, y' - y),
id ┴ ┴ └┘ └┘ ┴┴┴ └┘ └┘ ┴
src └─────────────────┘ └┘ └┘ ┴ └┘ └┘┴┴ ┴ ┴ └┘ └┘┴┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴
typ └─────────────────┘ └┘ └┘ ┴ └┘ └┘┴┴ ┴ ┴ └┘ └┘┴┴ └┘┴ ┴ └┘ ┴ ┴└┘└┘ ┴ └┘ ┴ ┴ └┘ ┴┴┴┴┴ ┴└┘└┘└┘┴ ┴┴┴
doc └─────────────────┘ └┘ └┘ ┴ └┘ └┘ ┴ ┴ ┴ └┘ └┘ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴
txt └─────────────────┘ └┘ └┘ ┴ └┘ └┘ ┴ ┴ ┴ └┘ └┘ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴
par └─────────────────┘ └┘ └┘ ┴ └┘ └┘ ┴ ┴ ┴ └┘ └┘ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴
pid └──────────────┘└─┘ └┘ └┘ ┴ └┘ └┘ ┴ ┴ ┴ └┘ └┘ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴
st ────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘└─
415 { repeat { rw is_Z_bilin.sub_left φ },
id └─────────────────┘ ┴
src └───────┘└─┘└─────────────────┘┴ ┴┴
typ └───────┘└─┘└─────────────────┘┴┴┴┴
doc └───────┘└─┘ ┴ ┴┴
txt └───────┘└─┘ ┴ ┴┴
par └───────┘└─┘ ┴ ┴┴
pid └────┘ ┴ └┘
st ───┘└────────────────────────────────┘└┘└
416 repeat { rw is_Z_bilin.sub_right φ },
id └──────────────────┘ ┴
src └───────┘└─┘└──────────────────┘┴ ┴┴
typ └───────┘└─┘└──────────────────┘┴┴┴┴
doc └───────┘└─┘ ┴ ┴┴
txt └───────┘└─┘ ┴ ┴┴
par └───────┘└─┘ ┴ ┴┴
pid └────┘ ┴ └┘
st ──────────────────────────────────────┘└┘└
417 apply eq_of_sub_eq_zero,
id └───────────────┘
src └────┘└───────────────┘
typ └────┘└───────────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ──────────────────────────┘└─
418 simp },
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
pid ┴
st ────────┘└┘└
419 rw key_formula,
id └─────────┘
src └─┘
typ └─┘└─────────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ───────────────┘└─
420 have h₁ := HU x x' xU₂ x'U₂,
id └┘ ┴ └┘ └─┘ └──┘
src └─────────┘ ┴ ┴ ┴ ┴
typ └─────────┘└┘┴┴┴└┘┴└─┘┴└──┘
doc └─────────┘ ┴ ┴ ┴ ┴
txt └─────────┘ ┴ ┴ ┴ ┴
par └─────────┘ ┴ ┴ ┴ ┴
pid └─────┘┴└─┘ ┴ ┴ ┴ ┴
st ────────────────────────────┘└─
421 have h₂ := H x x' xU₁ x'U₁ y₁ y' y₁_in y'V₁,
id ┴ ┴ └┘ └─┘ └──┘ └┘ └┘ └───┘ └──┘
src └─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ └─────────┘┴┴┴┴└┘┴└─┘┴└──┘┴└┘┴└┘┴└───┘┴└──┘
doc └─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
txt └─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
par └─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
pid └─────┘┴└─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
st ────────────────────────────────────────────┘└─
422 have h₃ := HV y y' yV₂ y'V₂,
id └┘ ┴ └┘ └─┘ └──┘
src └─────────┘ ┴ ┴ ┴ ┴
typ └─────────┘└┘┴┴┴└┘┴└─┘┴└──┘
doc └─────────┘ ┴ ┴ ┴ ┴
txt └─────────┘ ┴ ┴ ┴ ┴
par └─────────┘ ┴ ┴ ┴ ┴
pid └─────┘┴└─┘ ┴ ┴ ┴ ┴
st ────────────────────────────┘└─
423 have h₄ := H x₁ x x₁_in xU₁ y y' yV₁ y'V₁,
id ┴ └┘ ┴ └───┘ └─┘ ┴ └┘ └─┘ └──┘
src └─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ └─────────┘┴┴└┘┴┴┴└───┘┴└─┘┴┴┴└┘┴└─┘┴└──┘
doc └─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
txt └─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
par └─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
pid └─────┘┴└─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
st ──────────────────────────────────────────┘└─
424
st ─
425 exact W4 h₁ h₂ h₃ h₄
id └┘ └┘ └┘ └┘ └┘
src └────┘ ┴ ┴ ┴ ┴ ┴
typ └────┘└┘┴└┘┴└┘┴└┘┴└┘┴
doc └────┘ ┴ ┴ ┴ ┴ ┴
txt └────┘ ┴ ┴ ┴ ┴ ┴
par └────┘ ┴ ┴ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴ ┴ ┴
st ──────────────────────┘
426 end
st └─┘
427
428 omit W'_nhd
429
430 open dense_inducing
431
432 /-- Bourbaki GT III.6.5 Theorem I:
433 ℤ-bilinear continuous maps from dense images into a complete Hausdorff group extend by continuity.
434 Note: Bourbaki assumes that α and β are also complete Hausdorff, but this is not necessary. -/
435 theorem extend_Z_bilin : continuous (extend (de.prod df) φ) :=
id └────────┘ └────┘ └┘└───┘ └┘ ┴
src └────────┘ └────┘ └───┘
typ └────────┘ └────┘ └┘└───┘ └┘ ┴
doc └────────┘ └────┘ └───┘
436 begin
st └─────
437 refine continuous_extend_of_cauchy _ _,
id └─────────────────────────┘
src └─────┘└─────────────────────────┘└──┘
typ └─────┘└─────────────────────────┘└──┘
doc └─────┘ └──┘
txt └─────┘ └──┘
par └─────┘ └──┘
pid ┴ └──┘
st ───────────────────────────────────────┘└─
438 rintro ⟨x₀, y₀⟩,
src └─────────────┘
typ └─────────────┘
doc └─────────────┘
txt └─────────────┘
par └─────────────┘
pid └───────┘
st ────────────────┘└─
439 split,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
st ──────┘└─
440 { apply map_ne_bot,
id └────────┘
src └────┘└────────┘
typ └────┘└────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ───┘└──────────────┘└─
441 apply comap_ne_bot,
id └──────────┘
src └────┘└──────────┘
typ └────┘└──────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ─────────────────────┘└─
442
st ─
443 intros U h,
src └────────┘
typ └────────┘
doc └────────┘
txt └────────┘
par └────────┘
pid └──┘
st ─────────────┘└─
444 rcases mem_closure_iff_nhds.1 ((de.prod df).dense (x₀, y₀)) U h with ⟨x, x_in, ⟨z, z_x⟩⟩,
id └──────────────────┘ └─────┘ └┘ ┴└┘ └┘ ┴ ┴
src └─────┘└──────────────────┘└─┘ └─────┘┴ └──────┘┴ └┘ └─┘ ┴ └───────────────────────┘
typ └─────┘└──────────────────┘└─┘ └─────┘┴└┘└──────┘┴└┘└┘└┘└─┘┴┴┴└───────────────────────┘
doc └─────┘ └─┘ └─────┘┴ └──────┘ └┘ └─┘ ┴ └───────────────────────┘
txt └─────┘ └─┘ ┴ └──────┘ └┘ └─┘ ┴ └───────────────────────┘
par └─────┘ └─┘ ┴ └──────┘ └┘ └─┘ ┴ └───────────────────────┘
pid ┴ └─┘ ┴ └──────┘ └┘ └─┘ ┴ └───────────────────────┘
st ───────────────────────────────────────────────────────────────────────────────────────────┘└─
445 existsi z,
id ┴
src └──────┘
typ └──────┘┴
doc └──────┘
txt └──────┘
par └──────┘
pid ┴
st ────────────┘└─
446 cc },
src └─┘
typ └─┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ──────┘└┘└
447 { suffices : map (λ (p : (β × δ) × (β × δ)), φ p.2 - φ p.1)
id └─┘ ┴ ┴ ┴ ┴
src └─────────┘└─┘┴ └────┘ ┴┴┴ └┘ ┴ ┴ ┴ └──┘ ┴ └─┘┴┴ ┴ └───
typ └─────────┘└─┘┴ └────┘ ┴┴┴ └┘┴┴ ┴ ┴ └──┘ ┴ └─┘┴┴┴┴ └───
doc └─────────┘└─┘┴ └────┘ ┴ ┴ └┘ ┴ ┴ ┴ └──┘ ┴ └─┘ ┴ ┴ └───
txt └─────────┘ ┴ └────┘ ┴ ┴ └┘ ┴ ┴ ┴ └──┘ ┴ └─┘ ┴ ┴ └───
par └─────────┘ ┴ └────┘ ┴ ┴ └┘ ┴ ┴ ┴ └──┘ ┴ └─┘ ┴ ┴ └───
pid └───────┘└┘ ┴ └────┘ ┴ ┴ └┘ ┴ ┴ ┴ └──┘ ┴ └─┘ ┴ ┴ └───
st ──────────────────────────────────────────────────────────────
448 (comap (λ (p : (β × δ) × β × δ), ((e p.1.1, f p.1.2), (e p.2.1, f p.2.2)))
id └───┘ ┴ ┴ ┴ ┴
src ─────┘ └───┘┴ └────┘ ┴ ┴ └┘ ┴ ┴ ┴ └─┘ ┴ └────┘ ┴ └─────┘ ┴ └────┘ ┴ └───────
typ ─────┘ └───┘┴ └────┘ ┴ ┴ └┘ ┴┴┴ ┴┴└─┘ ┴ └────┘ ┴ └─────┘ ┴┴ └────┘┴┴ └───────
doc ─────┘ └───┘┴ └────┘ ┴ ┴ └┘ ┴ ┴ ┴ └─┘ ┴ └────┘ ┴ └─────┘ ┴ └────┘ ┴ └───────
txt ─────┘ ┴ └────┘ ┴ ┴ └┘ ┴ ┴ ┴ └─┘ ┴ └────┘ ┴ └─────┘ ┴ └────┘ ┴ └───────
par ─────┘ ┴ └────┘ ┴ ┴ └┘ ┴ ┴ ┴ └─┘ ┴ └────┘ ┴ └─────┘ ┴ └────┘ ┴ └───────
pid ─────┘ ┴ └────┘ ┴ ┴ └┘ ┴ ┴ ┴ └─┘ ┴ └────┘ ┴ └─────┘ ┴ └────┘ ┴ └───────
st ─────────────────────────────────────────────────────────────────────────────────
449 (filter.prod (𝓝 (x₀, y₀)) (𝓝 (x₀, y₀)))) ≤ 𝓝 0,
id └─────────┘ ┴ ┴└┘ └┘ ┴
src ────────┘ └─────────┘┴ ┴┴ └┘ └─┘ ┴┴ └┘ └───┘┴┴ └┘
typ ────────┘ └─────────┘┴ ┴┴ └┘ └─┘ ┴┴└┘└┘└┘└───┘┴┴ └┘
doc ────────┘ └─────────┘┴ ┴┴ └┘ └─┘ ┴ └┘ └───┘ ┴ └┘
txt ────────┘ ┴ ┴ └┘ └─┘ ┴ └┘ └───┘ ┴ └┘
par ────────┘ ┴ ┴ └┘ └─┘ ┴ └┘ └───┘ ┴ └┘
pid ────────┘ ┴ ┴ └┘ └─┘ ┴ └┘ └───┘ ┴ ┴┴
st ──────────────────────────────────────────────────────┘
450 by rwa [uniformity_eq_comap_nhds_zero G, prod_map_map_eq, ←map_le_iff_le_comap, filter.map_map,
id └───────────────────────────┘ ┴ └─────────────┘ └─────────────────┘ └────────────┘
src └───┘└───────────────────────────┘┴ └┘└─────────────┘└─┘└─────────────────┘└┘└────────────┘└─
typ └───┘└───────────────────────────┘┴┴└┘└─────────────┘└─┘└─────────────────┘└┘└────────────┘└─
doc └───┘ ┴ └┘ └─┘ └┘ └─
txt └───┘ ┴ └┘ └─┘ └┘ └─
par └───┘ ┴ └┘ └─┘ └┘ └─
pid └┘ ┴ └┘ └─┘ └┘ └─
st └─────────────────────────────┘└───────────────┘└────────────────────┘└──────────────┘└─
451 prod_comap_comap_eq],
id └─────────────────┘
src ───────┘└─────────────────┘┴
typ ───────┘└─────────────────┘┴
doc ───────┘ ┴
txt ───────┘ ┴
par ───────┘ ┴
pid ───────┘ ┴
st ──────────────────────────┘┴└─
452
st ─
453 intros W' W'_nhd,
src └──────────────┘
typ └──────────────┘
doc └──────────────┘
txt └──────────────┘
par └──────────────┘
pid └────────┘
st ───────────────────┘└─
454
st ─
455 have key := extend_Z_bilin_key de df hφ W'_nhd x₀ y₀,
id └────────────────┘ └┘ └┘ └┘ └────┘ └┘ └┘
src └──────────┘└────────────────┘┴ ┴ ┴ ┴ ┴ ┴
typ └──────────┘└────────────────┘┴└┘┴└┘┴└┘┴└────┘┴└┘┴└┘
doc └──────────┘ ┴ ┴ ┴ ┴ ┴ ┴
txt └──────────┘ ┴ ┴ ┴ ┴ ┴ ┴
par └──────────┘ ┴ ┴ ┴ ┴ ┴ ┴
pid └──────┘┴└─┘ ┴ ┴ ┴ ┴ ┴ ┴
st ───────────────────────────────────────────────────────┘└─
456 rcases key with ⟨U, U_nhd, V, V_nhd, h⟩,
id └─┘
src └─────┘ └───────────────────────────┘
typ └─────┘└─┘└───────────────────────────┘
doc └─────┘ └───────────────────────────┘
txt └─────┘ └───────────────────────────┘
par └─────┘ └───────────────────────────┘
pid ┴ └───────────────────────────┘
st ──────────────────────────────────────────┘└─
457 rw mem_comap_sets at U_nhd,
id └────────────┘
src └─┘└────────────┘└───────┘
typ └─┘└────────────┘└───────┘
doc └─┘ └───────┘
txt └─┘ └───────┘
par └─┘ └───────┘
pid ┴ └───────┘
st ─────────────────────────────┘└─
458 rcases U_nhd with ⟨U', U'_nhd, U'_sub⟩,
id └───┘
src └─────┘ └────────────────────────┘
typ └─────┘└───┘└────────────────────────┘
doc └─────┘ └────────────────────────┘
txt └─────┘ └────────────────────────┘
par └─────┘ └────────────────────────┘
pid ┴ └────────────────────────┘
st ─────────────────────────────────────────┘└─
459 rw mem_comap_sets at V_nhd,
id └────────────┘
src └─┘└────────────┘└───────┘
typ └─┘└────────────┘└───────┘
doc └─┘ └───────┘
txt └─┘ └───────┘
par └─┘ └───────┘
pid ┴ └───────┘
st ─────────────────────────────┘└─
460 rcases V_nhd with ⟨V', V'_nhd, V'_sub⟩,
id └───┘
src └─────┘ └────────────────────────┘
typ └─────┘└───┘└────────────────────────┘
doc └─────┘ └────────────────────────┘
txt └─────┘ └────────────────────────┘
par └─────┘ └────────────────────────┘
pid ┴ └────────────────────────┘
st ─────────────────────────────────────────┘└─
461
st ─
462 rw [mem_map, mem_comap_sets, nhds_prod_eq],
id └─────┘ └────────────┘ └──────────┘
src └──┘└─────┘└┘└────────────┘└┘└──────────┘┴
typ └──┘└─────┘└┘└────────────┘└┘└──────────┘┴
doc └──┘ └┘ └┘ ┴
txt └──┘ └┘ └┘ ┴
par └──┘ └┘ └┘ ┴
pid └┘ └┘ └┘ ┴
st ──────────────┘└──────────────┘└────────────┘└──
463 existsi set.prod (set.prod U' V') (set.prod U' V'),
id └──────┘ └┘ └┘
src └──────┘ ┴ ┴ ┴ └┘ └──────┘┴ ┴ ┴
typ └──────┘ ┴ ┴ ┴ └┘ └──────┘┴└┘┴└┘┴
doc └──────┘ ┴ ┴ ┴ └┘ └──────┘┴ ┴ ┴
txt └──────┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴
par └──────┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴
st ─────────────────────────────────────────────────────┘└─
464 rw mem_prod_same_iff,
id └───────────────┘
src └─┘└───────────────┘
typ └─┘└───────────────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ───────────────────────┘└─
465
st ─
466 simp only [exists_prop],
id └─────────┘
src └─────────┘└─────────┘┴
typ └─────────┘└─────────┘┴
doc └─────────┘ ┴
txt └─────────┘ ┴
par └─────────┘ ┴
pid ┴└──┘└┘ ┴
st ──────────────────────────┘└─
467 split,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
st ────────┘└─
468 { change U' ∈ 𝓝 x₀ at U'_nhd,
id └┘ ┴ └┘
src └─────┘ ┴┴┴ ┴ └────────┘
typ └─────┘└┘┴┴┴ ┴└┘└────────┘
doc └─────┘ ┴ ┴ ┴ └────────┘
txt └─────┘ ┴ ┴ ┴ └────────┘
par └─────┘ ┴ ┴ ┴ └────────┘
pid ┴ ┴ ┴ ┴ ┴└───────┘
st ─────┘└────────────────────────┘└─
469 change V' ∈ 𝓝 y₀ at V'_nhd,
id └┘ └┘
src └─────┘ ┴ ┴ ┴ └────────┘
typ └─────┘└┘┴ ┴ ┴└┘└────────┘
doc └─────┘ ┴ ┴ ┴ └────────┘
txt └─────┘ ┴ ┴ ┴ └────────┘
par └─────┘ ┴ ┴ ┴ └────────┘
pid ┴ ┴ ┴ ┴ ┴└───────┘
st ───────────────────────────────┘└─
470 have := prod_mem_prod U'_nhd V'_nhd,
id └───────────┘ └────┘ └────┘
src └──────┘└───────────┘┴ ┴
typ └──────┘└───────────┘┴└────┘┴└────┘
doc └──────┘ ┴ ┴
txt └──────┘ ┴ ┴
par └──────┘ ┴ ┴
pid └───┘└─┘ ┴ ┴
st ────────────────────────────────────────┘└─
471 tauto },
src └────┘
typ └────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ───────────┘└┘└
472 { intros p h',
src └─────────┘
typ └─────────┘
doc └─────────┘
txt └─────────┘
par └─────────┘
pid └───┘
st ────────────────┘└─
473 simp only [set.mem_preimage, set.prod_mk_mem_set_prod_eq] at h',
id └──────────────┘ └─────────────────────────┘
src └─────────┘└──────────────┘└┘└─────────────────────────┘└─────┘
typ └─────────┘└──────────────┘└┘└─────────────────────────┘└─────┘
doc └─────────┘ └┘ └─────┘
txt └─────────┘ └┘ └─────┘
par └─────────┘ └┘ └─────┘
pid ┴└──┘└┘ └┘ ┴┴└───┘
st ────────────────────────────────────────────────────────────────────┘└─
474 rcases p with ⟨⟨x, y⟩, ⟨x', y'⟩⟩,
id ┴
src └─────┘ └──────────────────────┘
typ └─────┘┴└──────────────────────┘
doc └─────┘ └──────────────────────┘
txt └─────┘ └──────────────────────┘
par └─────┘ └──────────────────────┘
pid ┴ └──────────────────────┘
st ─────────────────────────────────────┘└─
475 apply h ; tauto } }
src └────┘ ┴ └────┘
typ └────┘ ┴ └────┘
doc └────┘ ┴ └────┘
txt └────┘ ┴ └────┘
par └────┘ ┴ └────┘
pid ┴ ┴ ┴
st ─────────────────────┘└───
476 end
st ──┘
477 end dense_inducing